From Undecidability.L.Tactics Require Import LTactics GenEncode.
From Undecidability.L Require Import Functions.EqBool.
From Undecidability.L.Datatypes Require Import LBool LNat LOptions LProd.
From Undecidability.L Require Import UpToC.
From Undecidability.L.Datatypes.List Require List_enc.
Include List_enc.
From Undecidability.L.Datatypes.List Require Export List_basics List_eqb List_extra List_fold List_in List_nat.
Definition c__listsizeCons := 5.
Definition c__listsizeNil := 4.
Lemma size_list X `{registered X} (l:list X):
size (enc l) = sumn (map (fun x => size (enc x) + c__listsizeCons) l)+ c__listsizeNil.
Proof.
change (enc l) with (list_enc l). unfold c__listsizeCons, c__listsizeNil.
induction l.
-easy.
-cbn [list_enc map sumn size].
change ((match H with
| @mk_registered _ enc _ _ => enc
end a)) with (enc a). solverec.
Qed.
Lemma size_list_cons (X : Type) (H : registered X) x (l : list X):
size (enc (x::l)) = size (enc x) + size (enc l) + c__listsizeCons.
Proof.
rewrite !size_list. cbn. lia.
Qed.
Lemma size_rev X {_:registered X} (xs : list X): L_facts.size (enc (rev xs)) = L_facts.size (enc xs).
Proof.
rewrite !size_list,map_rev,<- sumn_rev. easy.
Qed.
Lemma size_list_In X {R__X :registered X} (x:X) xs:
x el xs -> L_facts.size (enc x) <= L_facts.size (enc xs).
Proof.
intro H. rewrite !size_list,sumn_map_add. rewrite <- (sumn_le_in (in_map _ _ _ H)) at 1. nia.
Qed.
Lemma size_list_enc_r {X} `{registered X} (l:list X):
length l <= size (enc l).
Proof.
rewrite size_list. induction l;cbn. all: unfold c__listsizeNil, c__listsizeCons in *; lia.
Qed.
From Undecidability.L Require Import Functions.EqBool.
From Undecidability.L.Datatypes Require Import LBool LNat LOptions LProd.
From Undecidability.L Require Import UpToC.
From Undecidability.L.Datatypes.List Require List_enc.
Include List_enc.
From Undecidability.L.Datatypes.List Require Export List_basics List_eqb List_extra List_fold List_in List_nat.
Definition c__listsizeCons := 5.
Definition c__listsizeNil := 4.
Lemma size_list X `{registered X} (l:list X):
size (enc l) = sumn (map (fun x => size (enc x) + c__listsizeCons) l)+ c__listsizeNil.
Proof.
change (enc l) with (list_enc l). unfold c__listsizeCons, c__listsizeNil.
induction l.
-easy.
-cbn [list_enc map sumn size].
change ((match H with
| @mk_registered _ enc _ _ => enc
end a)) with (enc a). solverec.
Qed.
Lemma size_list_cons (X : Type) (H : registered X) x (l : list X):
size (enc (x::l)) = size (enc x) + size (enc l) + c__listsizeCons.
Proof.
rewrite !size_list. cbn. lia.
Qed.
Lemma size_rev X {_:registered X} (xs : list X): L_facts.size (enc (rev xs)) = L_facts.size (enc xs).
Proof.
rewrite !size_list,map_rev,<- sumn_rev. easy.
Qed.
Lemma size_list_In X {R__X :registered X} (x:X) xs:
x el xs -> L_facts.size (enc x) <= L_facts.size (enc xs).
Proof.
intro H. rewrite !size_list,sumn_map_add. rewrite <- (sumn_le_in (in_map _ _ _ H)) at 1. nia.
Qed.
Lemma size_list_enc_r {X} `{registered X} (l:list X):
length l <= size (enc l).
Proof.
rewrite size_list. induction l;cbn. all: unfold c__listsizeNil, c__listsizeCons in *; lia.
Qed.