From b5f54d2815f446a999736abd0ffe80641596a5f6 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 11 Nov 2011 16:13:32 +0000 Subject: [PATCH] commit by user andrea --- weblib/Cerco/ASM/ASM.ma | 204 ++++++++ weblib/Cerco/ASM/BitVector.ma | 205 ++++++++ weblib/Cerco/ASM/FoldStuff.ma | 52 ++ weblib/Cerco/ASM/JMCoercions.ma | 23 + weblib/Cerco/ASM/Utils.ma | 897 ++++++++++++++++++++++++++++++++ weblib/basics/types.ma | 4 +- weblib/tutorial/chapter3.ma | 1 - weblib/tutorial/chapter4.ma | 577 +++++++++++++++++++- 8 files changed, 1954 insertions(+), 9 deletions(-) create mode 100644 weblib/Cerco/ASM/ASM.ma create mode 100644 weblib/Cerco/ASM/BitVector.ma create mode 100644 weblib/Cerco/ASM/FoldStuff.ma create mode 100644 weblib/Cerco/ASM/JMCoercions.ma create mode 100644 weblib/Cerco/ASM/Utils.ma diff --git a/weblib/Cerco/ASM/ASM.ma b/weblib/Cerco/ASM/ASM.ma new file mode 100644 index 000000000..437511f5a --- /dev/null +++ b/weblib/Cerco/ASM/ASM.ma @@ -0,0 +1,204 @@ +include "ASM/BitVector.ma". + +definition Identifier ≝ Word. + +inductive addressing_mode: Type[0] ≝ + DIRECT: Byte → addressing_mode +| INDIRECT: Bit → addressing_mode +| EXT_INDIRECT: Bit → addressing_mode +| REGISTER: BitVector 3 → addressing_mode +| ACC_A: addressing_mode +| ACC_B: addressing_mode +| DPTR: addressing_mode +| DATA: Byte → addressing_mode +| DATA16: Word → addressing_mode +| ACC_DPTR: addressing_mode +| ACC_PC: addressing_mode +| EXT_INDIRECT_DPTR: addressing_mode +| INDIRECT_DPTR: addressing_mode +| CARRY: addressing_mode +| BIT_ADDR: Byte → addressing_mode +| N_BIT_ADDR: Byte → addressing_mode +| RELATIVE: Byte → addressing_mode +| ADDR11: Word11 → addressing_mode +| ADDR16: Word → addressing_mode. + +(* dpm: renamed register to registr to avoid clash with brian's types *) +inductive addressing_mode_tag : Type[0] ≝ + direct: addressing_mode_tag +| indirect: addressing_mode_tag +| ext_indirect: addressing_mode_tag +| registr: addressing_mode_tag +| acc_a: addressing_mode_tag +| acc_b: addressing_mode_tag +| dptr: addressing_mode_tag +| data: addressing_mode_tag +| data16: addressing_mode_tag +| acc_dptr: addressing_mode_tag +| acc_pc: addressing_mode_tag +| ext_indirect_dptr: addressing_mode_tag +| indirect_dptr: addressing_mode_tag +| carry: addressing_mode_tag +| bit_addr: addressing_mode_tag +| n_bit_addr: addressing_mode_tag +| relative: addressing_mode_tag +| addr11: addressing_mode_tag +| addr16: addressing_mode_tag. + +definition eq_a ≝ + λa, b: addressing_mode_tag. + match a with + [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ] + | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ] + | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ] + | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ] + | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ] + | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ] + | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ] + | data ⇒ match b with [ data ⇒ true | _ ⇒ false ] + | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ] + | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ] + | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ] + | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ] + | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ] + | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ] + | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ] + | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ] + | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ] + | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ] + | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ] + ]. + +(* to avoid expansion... *) +let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝ + match d with + [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ] + | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ] + | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ] + | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ] + | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ] + | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ] + | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ] + | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ] + | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ] + | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ] + | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ] + | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ] + | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ] + | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ] + | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ] + | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ] + | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ] + | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ] + | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ] + ]. + + +let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝ + match l return λm.λ_:Vector addressing_mode_tag m.bool with + [ VEmpty ⇒ false + | VCons m he (tl: Vector addressing_mode_tag m) ⇒ + is_a he A ∨ is_in ? tl A ]. + +record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝ +{ + subaddressing_modeel:> addressing_mode; + subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) +}. + +coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0] + ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0]. + +coercion mk_subaddressing_mode : + ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode. + ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l + ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?. + +inductive preinstruction (A: Type[0]) : Type[0] ≝ + ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A +| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A +| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A +| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A +| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A +| MUL: [[acc_a]] → [[acc_b]] → preinstruction A +| DIV: [[acc_a]] → [[acc_b]] → preinstruction A +| DA: [[acc_a]] → preinstruction A + +(* conditional jumps *) +| JC: A → preinstruction A +| JNC: A → preinstruction A +| JB: [[bit_addr]] → A → preinstruction A +| JNB: [[bit_addr]] → A → preinstruction A +| JBC: [[bit_addr]] → A → preinstruction A +| JZ: A → preinstruction A +| JNZ: A → preinstruction A +| CJNE: + [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A +| DJNZ: [[registr ; direct]] → A → preinstruction A + (* logical operations *) +| ANL: + [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ + [[direct]] × [[ acc_a ; data ]] ⊎ + [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A +| ORL: + [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎ + [[direct]] × [[ acc_a ; data ]] ⊎ + [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A +| XRL: + [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎ + [[direct]] × [[ acc_a ; data ]] → preinstruction A +| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A +| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A +| RL: [[acc_a]] → preinstruction A +| RLC: [[acc_a]] → preinstruction A +| RR: [[acc_a]] → preinstruction A +| RRC: [[acc_a]] → preinstruction A +| SWAP: [[acc_a]] → preinstruction A + + (* data transfer *) +| MOV: + [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ + [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎ + [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎ + [[dptr]] × [[data16]] ⊎ + [[carry]] × [[bit_addr]] ⊎ + [[bit_addr]] × [[carry]] → preinstruction A +| MOVX: + [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎ + [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A +| SETB: [[ carry ; bit_addr ]] → preinstruction A +| PUSH: [[direct]] → preinstruction A +| POP: [[direct]] → preinstruction A +| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A +| XCHD: [[acc_a]] → [[indirect]] → preinstruction A + + (* program branching *) +| RET: preinstruction A +| RETI: preinstruction A +| NOP: preinstruction A. + +inductive instruction: Type[0] ≝ + | ACALL: [[addr11]] → instruction + | LCALL: [[addr16]] → instruction + | AJMP: [[addr11]] → instruction + | LJMP: [[addr16]] → instruction + | SJMP: [[relative]] → instruction + | JMP: [[indirect_dptr]] → instruction + | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction + | RealInstruction: preinstruction [[ relative ]] → instruction. + +coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝ + RealInstruction on _p: preinstruction ? to instruction. + +inductive pseudo_instruction: Type[0] ≝ + | Instruction: preinstruction Identifier → pseudo_instruction + | Comment: String → pseudo_instruction + | Cost: Identifier → pseudo_instruction + | Jmp: Identifier → pseudo_instruction + | Call: Identifier → pseudo_instruction + | Mov: [[dptr]] → Identifier → pseudo_instruction. + +definition labelled_instruction ≝ option Identifier × pseudo_instruction. +definition preamble ≝ list (Identifier × nat). +definition assembly_program ≝ list instruction. +definition pseudo_assembly_program ≝ preamble × (list labelled_instruction). diff --git a/weblib/Cerco/ASM/BitVector.ma b/weblib/Cerco/ASM/BitVector.ma new file mode 100644 index 000000000..98f68e8af --- /dev/null +++ b/weblib/Cerco/ASM/BitVector.ma @@ -0,0 +1,205 @@ +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* BitVector.ma: Fixed length bitvectors, and common operations on them. *) +(* Most functions are specialised versions of those found in *) +(* Vector.ma as a courtesy, or boolean functions lifted into *) +(* BitVector variants. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +include "arithmetics/nat.ma". + +include "ASM/FoldStuff.ma". +include "ASM/Vector.ma". +include "ASM/String.ma". + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Common synonyms. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +definition BitVector ≝ λn: nat. Vector bool n. +definition Bit ≝ bool. +definition Nibble ≝ BitVector 4. +definition Byte7 ≝ BitVector 7. +definition Byte ≝ BitVector 8. +definition Word ≝ BitVector 16. +definition Word11 ≝ BitVector 11. + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Inversion *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. + #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // + #n #hd #tl #abs @⊥ destruct (abs) +qed. + +lemma BitVector_Sn: ∀n.∀v:BitVector (S n). + ∃hd.∃tl.v ≃ VCons bool n hd tl. + #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) + [ #abs @⊥ destruct (abs) + | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] +qed. + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Lookup. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Creating bitvectors from scratch. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +definition zero: ∀n:nat. BitVector n ≝ + λn: nat. replicate bool n false. + +definition maximum: ∀n:nat. BitVector n ≝ + λn: nat. replicate bool n true. + +definition pad ≝ + λm, n: nat. + λb: BitVector n. pad_vector ? false m n b. + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Other manipulations. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Logical operations. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝ + λn: nat. + λb: BitVector n. + λc: BitVector n. + zip_with ? ? ? n (andb) b c. + +interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c). + +definition inclusive_disjunction_bv ≝ + λn: nat. + λb: BitVector n. + λc: BitVector n. + zip_with ? ? ? n (orb) b c. + +interpretation "BitVector inclusive disjunction" + 'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c). + +definition exclusive_disjunction_bv ≝ + λn: nat. + λb: BitVector n. + λc: BitVector n. + zip_with ? ? ? n (exclusive_disjunction) b c. + +interpretation "BitVector exclusive disjunction" + 'exclusive_disjunction b c = (exclusive_disjunction ? b c). + +definition negation_bv ≝ + λn: nat. + λb: BitVector n. + map bool bool n (notb) b. + +interpretation "BitVector negation" 'negation b c = (negation_bv ? b c). + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Rotates and shifts. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) +(* Conversions to and from lists and natural numbers. *) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) + +definition eq_b ≝ + λb, c: bool. + if b then + c + else + notb c. + +lemma eq_b_eq: + ∀b, c. + eq_b b c = true → b = c. + #b #c + cases b + cases c + normalize // +qed. + +definition eq_bv ≝ + λn: nat. + λb, c: BitVector n. + eq_v bool n eq_b b c. + +lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y. + (x = y → P true) → + (x ≠ y → P false) → + P (eq_bv n x y). +#P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf) +#Q * *; normalize /3/ +qed. + +lemma eq_bv_true: ∀n,v. eq_bv n v v = true. +@eq_v_true * @refl +qed. + +lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false. +#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ] +qed. + +lemma eq_bv_refl: + ∀n,v. eq_bv n v v = true. + #n #v + elim v + [ // + | #n #hd #tl #ih + normalize + cases hd + [ normalize + @ ih + | normalize + @ ih + ] + ] +qed. + +lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1. + #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/] +qed. + +lemma eq_eq_bv: + ∀n, v, q. + v = q → eq_bv n v q = true. + #n #v + elim v + [ #q #h h normalize="" %="" |="" #n="" #hd="" #tl="" #ih="" #q="" #h=""h // + ] +qed. + +lemma eq_bv_eq: + ∀n, v, q. + eq_bv n v q = true → v = q. + #n #v #q generalize in match v + elim q + [ #v #h @BitVector_O + | #n #hd #tl #ih #v' #h + cases (BitVector_Sn ? v') + #hd' * #tl' #jmeq >jmeq in h; + #new_h + change in new_h with ((andb ? ?) = ?); + cases(conjunction_true … new_h) + #eq_heads #eq_tails + whd in eq_heads:(??(??(%))?); + cases(eq_b_eq … eq_heads) + whd in eq_tails:(??(?????(%))?); + change in eq_tails with (eq_bv ??? = ?); + <(ih tl') // + ] +qed. + +axiom bitvector_of_string: + ∀n: nat. + ∀s: String. + BitVector n. + +axiom string_of_bitvector: + ∀n: nat. + ∀b: BitVector n. + String. +/h \ No newline at end of file diff --git a/weblib/Cerco/ASM/FoldStuff.ma b/weblib/Cerco/ASM/FoldStuff.ma new file mode 100644 index 000000000..a2b3a4563 --- /dev/null +++ b/weblib/Cerco/ASM/FoldStuff.ma @@ -0,0 +1,52 @@ +include "ASM/Util.ma". +include "ASM/JMCoercions.ma". + +let rec foldl_strong_internal + (A: Type[0]) (P: list A → Type[0]) (l: list A) + (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd])) + (prefix: list A) (suffix: list A) (acc: P prefix) on suffix: + l = prefix @ suffix → P(prefix @ suffix) ≝ + match suffix return λl'. l = prefix @ l' → P (prefix @ l') with + [ nil ⇒ λprf. ? + | cons hd tl ⇒ λprf. ? + ]. + [ > (append_nil ?) + @ acc + | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?) + [ @ (H prefix hd tl prf acc) + | applyS prf + ] + ] +qed. + +definition foldl_strong ≝ + λA: Type[0]. + λP: list A → Type[0]. + λl: list A. + λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). + λacc: P [ ]. + foldl_strong_internal A P l H [ ] l acc (refl …). + +let rec foldr_strong_internal + (A:Type[0]) + (P: list A → Type[0]) + (l: list A) + (H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl)) + (prefix: list A) (suffix: list A) (acc: P [ ]) on suffix : l = prefix@suffix → P suffix ≝ + match suffix return λl'. l = prefix @ l' → P (l') with + [ nil ⇒ λprf. acc + | cons hd tl ⇒ λprf. H prefix hd tl prf (foldr_strong_internal A P l H (prefix @ [hd]) tl acc ?) ]. + applyS prf +qed. + +lemma foldr_strong: + ∀A:Type[0]. + ∀P: list A → Type[0]. + ∀l: list A. + ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl). + ∀acc:P [ ]. P l + ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …). + +lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2. + #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/ +qed. diff --git a/weblib/Cerco/ASM/JMCoercions.ma b/weblib/Cerco/ASM/JMCoercions.ma new file mode 100644 index 000000000..3f43e6b70 --- /dev/null +++ b/weblib/Cerco/ASM/JMCoercions.ma @@ -0,0 +1,23 @@ +include "basics/jmeq.ma". +include "basics/types.ma". +include "basics/list.ma". + +definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p. +definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w]. + +coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?. +coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?. + +(*axiom VOID: Type[0]. +axiom assert_false: VOID. +definition bigbang: ∀A:Type[0].False → VOID → A. + #A #abs cases abs +qed. + +coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*) + +lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p). + #A #P #p cases p #w #q @q +qed. + +(* END RUSSELL **) diff --git a/weblib/Cerco/ASM/Utils.ma b/weblib/Cerco/ASM/Utils.ma new file mode 100644 index 000000000..a7eeaad70 --- /dev/null +++ b/weblib/Cerco/ASM/Utils.ma @@ -0,0 +1,897 @@ +include "basics/list.ma". +include "basics/types.ma". +include "arithmetics/nat.ma". + +include "utilities/pair.ma". +include "ASM/JMCoercions.ma". + +(* let's implement a daemon not used by automation *) +inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX. +axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX. +example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed. +example not_implemented: False. cases daemon qed. + +notation "⊥" with precedence 90 + for @{ match ? in False with [ ] }. + +definition ltb ≝ + λm, n: nat. + leb (S m) n. + +definition geb ≝ + λm, n: nat. + ltb n m. + +definition gtb ≝ + λm, n: nat. + ltb n m. + +(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *) +let rec eq_nat (n: nat) (m: nat) on n: bool ≝ + match n with + [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ] + | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ] + ]. + +let rec forall + (A: Type[0]) (f: A → bool) (l: list A) + on l ≝ + match l with + [ nil ⇒ true + | cons hd tl ⇒ f hd ∧ forall A f tl + ]. + +let rec prefix + (A: Type[0]) (k: nat) (l: list A) + on l ≝ + match l with + [ nil ⇒ [ ] + | cons hd tl ⇒ + match k with + [ O ⇒ [ ] + | S k' ⇒ hd :: prefix A k' tl + ] + ]. + +let rec fold_left2 + (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A) + (left: list B) (right: list C) (proof: |left| = |right|) + on left: A ≝ + match left return λx. |x| = |right| → A with + [ nil ⇒ λnil_prf. + match right return λx. |[ ]| = |x| → A with + [ nil ⇒ λnil_nil_prf. accu + | cons hd tl ⇒ λcons_nil_absrd. ? + ] nil_prf + | cons hd tl ⇒ λcons_prf. + match right return λx. |hd::tl| = |x| → A with + [ nil ⇒ λcons_nil_absrd. ? + | cons hd' tl' ⇒ λcons_cons_prf. + fold_left2 … f (f accu hd hd') tl tl' ? + ] cons_prf + ] proof. + [ 1: normalize in cons_nil_absrd; + destruct(cons_nil_absrd) + | 2: normalize in cons_nil_absrd; + destruct(cons_nil_absrd) + | 3: normalize in cons_cons_prf; + @injective_S + assumption + ] +qed. + +let rec remove_n_first_internal + (i: nat) (A: Type[0]) (l: list A) (n: nat) + on l ≝ + match l with + [ nil ⇒ [ ] + | cons hd tl ⇒ + match eq_nat i n with + [ true ⇒ l + | _ ⇒ remove_n_first_internal (S i) A tl n + ] + ]. + +definition remove_n_first ≝ + λA: Type[0]. + λn: nat. + λl: list A. + remove_n_first_internal 0 A l n. + +let rec foldi_from_until_internal + (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A) + on rem ≝ + match rem with + [ nil ⇒ res + | cons e tl ⇒ + match geb i m with + [ true ⇒ res + | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f + ] + ]. + +definition foldi_from_until ≝ + λA: Type[0]. + λn: nat. + λm: nat. + λf: ?. + λa: ?. + λl: ?. + foldi_from_until_internal A 0 a (remove_n_first A n l) m f. + +definition foldi_from ≝ + λA: Type[0]. + λn. + λf. + λa. + λl. + foldi_from_until A n (|l|) f a l. + +definition foldi_until ≝ + λA: Type[0]. + λm. + λf. + λa. + λl. + foldi_from_until A 0 m f a l. + +definition foldi ≝ + λA: Type[0]. + λf. + λa. + λl. + foldi_from_until A 0 (|l|) f a l. + +definition hd_safe ≝ + λA: Type[0]. + λl: list A. + λproof: 0 < |l|. + match l return λx. 0 < |x| → A with + [ nil ⇒ λnil_absrd. ? + | cons hd tl ⇒ λcons_prf. hd + ] proof. + normalize in nil_absrd; + cases(not_le_Sn_O 0) + #HYP + cases(HYP nil_absrd) +qed. + +definition tail_safe ≝ + λA: Type[0]. + λl: list A. + λproof: 0 < |l|. + match l return λx. 0 < |x| → list A with + [ nil ⇒ λnil_absrd. ? + | cons hd tl ⇒ λcons_prf. tl + ] proof. + normalize in nil_absrd; + cases(not_le_Sn_O 0) + #HYP + cases(HYP nil_absrd) +qed. + +let rec split + (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|) + on index ≝ + match index return λx. x ≤ |l| → (list A) × (list A) with + [ O ⇒ λzero_prf. 〈[], l〉 + | S index' ⇒ λsucc_prf. + match l return λx. S index' ≤ |x| → (list A) × (list A) with + [ nil ⇒ λnil_absrd. ? + | cons hd tl ⇒ λcons_prf. + let 〈l1, l2〉 ≝ split A tl index' ? in + 〈hd :: l1, l2〉 + ] succ_prf + ] proof. + [1: normalize in nil_absrd; + cases(not_le_Sn_O index') + #HYP + cases(HYP nil_absrd) + |2: normalize in cons_prf; + @le_S_S_to_le + assumption + ] +qed. + +let rec nth_safe + (elt_type: Type[0]) (index: nat) (the_list: list elt_type) + (proof: index < | the_list |) + on index ≝ + match index return λs. s < | the_list | → elt_type with + [ O ⇒ + match the_list return λt. 0 < | t | → elt_type with + [ nil ⇒ λnil_absurd. ? + | cons hd tl ⇒ λcons_proof. hd + ] + | S index' ⇒ + match the_list return λt. S index' < | t | → elt_type with + [ nil ⇒ λnil_absurd. ? + | cons hd tl ⇒ + λcons_proof. nth_safe elt_type index' tl ? + ] + ] proof. + [ normalize in nil_absurd; + cases (not_le_Sn_O 0) + #ABSURD + elim (ABSURD nil_absurd) + | normalize in nil_absurd; + cases (not_le_Sn_O (S index')) + #ABSURD + elim (ABSURD nil_absurd) + | normalize in cons_proof + @le_S_S_to_le + assumption + ] +qed. + +definition last_safe ≝ + λelt_type: Type[0]. + λthe_list: list elt_type. + λproof : 0 < | the_list |. + nth_safe elt_type (|the_list| - 1) the_list ?. + normalize /2/ +qed. + +let rec reduce + (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝ + match left with + [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 + | cons hd tl ⇒ + match right with + [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 + | cons hd' tl' ⇒ + let 〈cleft, cright〉 ≝ reduce A B tl tl' in + let 〈commonl, restl〉 ≝ cleft in + let 〈commonr, restr〉 ≝ cright in + 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉 + ] + ]. + +(* +axiom reduce_strong: + ∀A: Type[0]. + ∀left: list A. + ∀right: list A. + Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |. +*) + +let rec reduce_strong + (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) + on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)| ≝ + match left with + [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 + | cons hd tl ⇒ + match right with + [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 + | cons hd' tl' ⇒ + let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in + let 〈commonl, restl〉 ≝ cleft in + let 〈commonr, restr〉 ≝ cright in + 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉 + ] + ]. + [ 1: normalize % + | 2: normalize % + | 3: normalize + generalize in match (sig2 … (reduce_strong A B tl tl1)); + >p2 >p3 >p4 normalize in ⊢ (% → ?) + #HYP // + ] +qed. + +let rec map2_opt + (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) + (left: list A) (right: list B) on left ≝ + match left with + [ nil ⇒ + match right with + [ nil ⇒ Some ? (nil C) + | _ ⇒ None ? + ] + | cons hd tl ⇒ + match right with + [ nil ⇒ None ? + | cons hd' tl' ⇒ + match map2_opt A B C f tl tl' with + [ None ⇒ None ? + | Some tail ⇒ Some ? (f hd hd' :: tail) + ] + ] + ]. + +let rec map2 + (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) + (left: list A) (right: list B) (proof: | left | = | right |) on left ≝ + match left return λx. | x | = | right | → list C with + [ nil ⇒ + match right return λy. | [] | = | y | → list C with + [ nil ⇒ λnil_prf. nil C + | _ ⇒ λcons_absrd. ? + ] + | cons hd tl ⇒ + match right return λy. | hd::tl | = | y | → list C with + [ nil ⇒ λnil_absrd. ? + | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ? + ] + ] proof. + [1: normalize in cons_absrd; + destruct(cons_absrd) + |2: normalize in nil_absrd; + destruct(nil_absrd) + |3: normalize in cons_prf; + destruct(cons_prf) + assumption + ] +qed. + +let rec map3 + (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D) + (left: list A) (centre: list B) (right: list C) + (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝ + match left return λx. |x| = |centre| → list D with + [ nil ⇒ λnil_prf. + match centre return λx. |x| = |right| → list D with + [ nil ⇒ λnil_nil_prf. + match right return λx. |nil ?| = |x| → list D with + [ nil ⇒ λnil_nil_nil_prf. nil D + | cons hd tl ⇒ λcons_nil_nil_absrd. ? + ] nil_nil_prf + | cons hd tl ⇒ λnil_cons_absrd. ? + ] prfcr + | cons hd tl ⇒ λcons_prf. + match centre return λx. |x| = |right| → list D with + [ nil ⇒ λcons_nil_absrd. ? + | cons hd' tl' ⇒ λcons_cons_prf. + match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with + [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ? + | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf. + (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?) + ] (refl ? (|right|)) cons_cons_prf + ] prfcr + ] prflc. + [ 1: normalize in cons_nil_nil_absrd; + destruct(cons_nil_nil_absrd) + | 2: generalize in match nil_cons_absrd; + prfcrnil_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" |="" 3:="" generalize="" in="" match="" cons_nil_absrd;=""prfcrcons_prf #hyp="" hyp;="" destruct(hyp)="" 4:="" cons_cons_nil_absrd;="" destruct(cons_cons_nil_absrd)="" 5:="" normalize="" destruct(cons_cons_cons_prf)="" assumption="" |="" 6:="" generalize="" in="" match="" cons_cons_cons_prf;=""refl_prfprfcrcons_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" @sym_eq="" assumption="" ]="" lemma="" eq_rect_type0_r="" :="" ∀a:="" ∀a:a.="" ∀p:="" ∀x:a.="" eq="" type[0].="" (refl="" a="" →="" ∀x:="" a.∀p:eq="" ?="" a.="" x="" p.="" #a="" #h="" #x="" #p="" h="" generalize="" in="" match="" cases="" p="" qed.="" let="" rec="" safe_nth="" (a:="" type[0])="" (n:="" nat)="" (l:="" list="" a)="" (p:="" n=""< length A l) on n: A ≝ + match n return λo. o < length A l → A with + [ O ⇒ + match l return λm. 0 < length A m → A with + [ nil ⇒ λabsd1. ? + | cons hd tl ⇒ λprf1. hd + ] + | S n' ⇒ + match l return λm. S n' < length A m → A with + [ nil ⇒ λabsd2. ? + | cons hd tl ⇒ λprf2. safe_nth A n' tl ? + ] + ] ?. + [ 1: + @ p + | 4: + normalize in prf2 + normalize + @ le_S_S_to_le + assumption + | 2: + normalize in absd1; + cases (not_le_Sn_O O) + # H + elim (H absd1) + | 3: + normalize in absd2; + cases (not_le_Sn_O (S n')) + # H + elim (H absd2) + ] +qed. + +let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝ + match n with + [ O ⇒ + match l with + [ nil ⇒ [ ] + | cons hd tl ⇒ l + ] + | S n ⇒ + match l with + [ nil ⇒ [ ] + | cons hd tl ⇒ + hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n + ] + ]. + +definition nub_by ≝ + λA: Type[0]. + λf: A → A → bool. + λl: list A. + nub_by_internal A f l (length ? l). + +let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝ + match l with + [ nil ⇒ false + | cons hd tl ⇒ orb (eq a hd) (member A eq a tl) + ]. + +let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝ + match n with + [ O ⇒ [ ] + | S n ⇒ + match l with + [ nil ⇒ [ ] + | cons hd tl ⇒ hd :: take A n tl + ] + ]. + +let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝ + match n with + [ O ⇒ l + | S n ⇒ + match l with + [ nil ⇒ [ ] + | cons hd tl ⇒ drop A n tl + ] + ]. + +definition list_split ≝ + λA: Type[0]. + λn: nat. + λl: list A. + 〈take A n l, drop A n l〉. + +let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B) + (l: list A) on l: list B ≝ + match l with + [ nil ⇒ nil ? + | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl) + ]. + +definition mapi ≝ + λA, B: Type[0]. + λf: nat → A → B. + λl: list A. + mapi_internal A B 0 f l. + +let rec zip_pottier + (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) + on left ≝ + match left with + [ nil ⇒ [ ] + | cons hd tl ⇒ + match right with + [ nil ⇒ [ ] + | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl' + ] + ]. + +let rec zip_safe + (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|) + on left ≝ + match left return λx. |x| = |right| → list (A × B) with + [ nil ⇒ λnil_prf. + match right return λx. |[ ]| = |x| → list (A × B) with + [ nil ⇒ λnil_nil_prf. [ ] + | cons hd tl ⇒ λnil_cons_absrd. ? + ] nil_prf + | cons hd tl ⇒ λcons_prf. + match right return λx. |hd::tl| = |x| → list (A × B) with + [ nil ⇒ λcons_nil_absrd. ? + | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ? + ] cons_prf + ] prf. + [ 1: normalize in nil_cons_absrd; + destruct(nil_cons_absrd) + | 2: normalize in cons_nil_absrd; + destruct(cons_nil_absrd) + | 3: normalize in cons_cons_prf; + @injective_S + assumption + ] +qed. + +let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝ + match l with + [ nil ⇒ Some ? (nil (A × B)) + | cons hd tl ⇒ + match r with + [ nil ⇒ None ? + | cons hd' tl' ⇒ + match zip ? ? tl tl' with + [ None ⇒ None ? + | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail) + ] + ] + ]. + +let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝ + match l with + [ nil ⇒ a + | cons hd tl ⇒ foldl A B f (f a hd) tl + ]. + +lemma foldl_step: + ∀A:Type[0]. + ∀B: Type[0]. + ∀H: A → B → A. + ∀acc: A. + ∀pre: list B. + ∀hd:B. + foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd). + #A #B #H #acc #pre generalize in match acc; -acc; elim pre + [ normalize; // + | #hd #tl #IH #acc #X normalize; @IH ] +qed. + +lemma foldl_append: + ∀A:Type[0]. + ∀B: Type[0]. + ∀H: A → B → A. + ∀acc: A. + ∀suff,pre: list B. + foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff). + #A #B #H #acc #suff elim suff + [ #pre >append_nil % + | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ] +qed. + +definition flatten ≝ + λA: Type[0]. + λl: list (list A). + foldr ? ? (append ?) [ ] l. + +let rec rev (A: Type[0]) (l: list A) on l ≝ + match l with + [ nil ⇒ nil A + | cons hd tl ⇒ (rev A tl) @ [ hd ] + ]. + +lemma append_length: + ∀A: Type[0]. + ∀l, r: list A. + |(l @ r)| = |l| + |r|. + #A #L #R + elim L + [ % + | #HD #TL #IH + normalize >IH % + ] +qed. + +lemma append_nil: + ∀A: Type[0]. + ∀l: list A. + l @ [ ] = l. + #A #L + elim L // +qed. + +lemma rev_append: + ∀A: Type[0]. + ∀l, r: list A. + rev A (l @ r) = rev A r @ rev A l. + #A #L #R + elim L + [ normalize >append_nil % + | #HD #TL #IH + normalize >IH + @associative_append + ] +qed. + +lemma rev_length: + ∀A: Type[0]. + ∀l: list A. + |rev A l| = |l|. + #A #L + elim L + [ % + | #HD #TL #IH + normalize + >(append_length A (rev A TL) [HD]) + normalize /2/ + ] +qed. + +lemma nth_append_first: + ∀A:Type[0]. + ∀n:nat.∀l1,l2:list A.∀d:A. + n < |l1| → nth n A (l1@l2) d = nth n A l1 d. + #A #n #l1 #l2 #d + generalize in match n; -n; elim l1 + [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O + | #h #t #Hind #k normalize + cases k -k + [ #Hk normalize @refl + | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk + ] + ] +qed. + +lemma nth_append_second: + ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 -> + nth n A (l1@l2) d = nth (n - length A l1) A l2 d. + #A #n #l1 #l2 #d + generalize in match n; -n; elim l1 + [ normalize #k #Hk <(minus_n_O) @refl + | #h #t #Hind #k normalize + cases k -k; + [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ] + | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk + ] + ] +qed. + + +notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 + for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }. +notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19 + for @{ match $e with [ true ⇒ $t | false ⇒ $f] }. + +let rec fold_left_i_aux (A: Type[0]) (B: Type[0]) + (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝ + match l with + [ nil ⇒ x + | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl + ]. + +definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. + +notation "hvbox(t⌈o ↦ h⌉)" + with precedence 45 + for @{ match (? : $o=$h) with [ refl ⇒ $t ] }. + +definition function_apply ≝ + λA, B: Type[0]. + λf: A → B. + λa: A. + f a. + +notation "f break $ x" + left associative with precedence 99 + for @{ 'function_apply $f $x }. + +interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). + +let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝ + match n with + [ O ⇒ a + | S o ⇒ f (iterate A f a o) + ]. + +(* Yeah, I probably ought to do something more general... *) +notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)" +with precedence 90 for @{ 'triple $a $b $c}. +interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z). + +notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)" +with precedence 90 for @{ 'quadruple $a $b $c $d}. +interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)). + +notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)" + with precedence 10 +for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }. + +notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)" + with precedence 10 +for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }. + +notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)" + with precedence 10 +for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }. + +axiom pair_elim': + ∀A,B,C: Type[0]. + ∀T: A → B → C. + ∀p. + ∀P: A×B → C → Prop. + (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) → + P p (let 〈lft, rgt〉 ≝ p in T lft rgt). + +axiom pair_elim'': + ∀A,B,C,C': Type[0]. + ∀T: A → B → C. + ∀T': A → B → C'. + ∀p. + ∀P: A×B → C → C' → Prop. + (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) → + P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt). + +lemma pair_destruct_1: + ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c. + #A #B #a #b *; /2/ +qed. + +lemma pair_destruct_2: + ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c. + #A #B #a #b *; /2/ +qed. + + +let rec exclusive_disjunction (b: bool) (c: bool) on b ≝ + match b with + [ true ⇒ + match c with + [ false ⇒ true + | true ⇒ false + ] + | false ⇒ + match c with + [ false ⇒ false + | true ⇒ true + ] + ]. + +(* dpm: conflicts with library definitions +interpretation "Nat less than" 'lt m n = (ltb m n). +interpretation "Nat greater than" 'gt m n = (gtb m n). +interpretation "Nat greater than eq" 'geq m n = (geb m n). +*) + +let rec division_aux (m: nat) (n : nat) (p: nat) ≝ + match ltb n (S p) with + [ true ⇒ O + | false ⇒ + match m with + [ O ⇒ O + | (S q) ⇒ S (division_aux q (n - (S p)) p) + ] + ]. + +definition division ≝ + λm, n: nat. + match n with + [ O ⇒ S m + | S o ⇒ division_aux m m o + ]. + +notation "hvbox(n break ÷ m)" + right associative with precedence 47 + for @{ 'division $n $m }. + +interpretation "Nat division" 'division n m = (division n m). + +let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝ + match leb n p with + [ true ⇒ n + | false ⇒ + match m with + [ O ⇒ n + | S o ⇒ modulus_aux o (n - (S p)) p + ] + ]. + +definition modulus ≝ + λm, n: nat. + match n with + [ O ⇒ m + | S o ⇒ modulus_aux m m o + ]. + +notation "hvbox(n break 'mod' m)" + right associative with precedence 47 + for @{ 'modulus $n $m }. + +interpretation "Nat modulus" 'modulus m n = (modulus m n). + +definition divide_with_remainder ≝ + λm, n: nat. + pair ? ? (m ÷ n) (modulus m n). + +let rec exponential (m: nat) (n: nat) on n ≝ + match n with + [ O ⇒ S O + | S o ⇒ m * exponential m o + ]. + +interpretation "Nat exponential" 'exp n m = (exponential n m). + +notation "hvbox(a break ⊎ b)" + left associative with precedence 50 +for @{ 'disjoint_union $a $b }. +interpretation "sum" 'disjoint_union A B = (Sum A B). + +theorem less_than_or_equal_monotone: + ∀m, n: nat. + m ≤ n → (S m) ≤ (S n). + #m #n #H + elim H + /2/ +qed. + +theorem less_than_or_equal_b_complete: + ∀m, n: nat. + leb m n = false → ¬(m ≤ n). + #m; + elim m; + normalize + [ #n #H + destruct + | #y #H1 #z + cases z + normalize + [ #H + /2/ + | /3/ + ] + ] +qed. + +theorem less_than_or_equal_b_correct: + ∀m, n: nat. + leb m n = true → m ≤ n. + #m + elim m + // + #y #H1 #z + cases z + normalize + [ #H + destruct + | #n #H lapply (H1 … H) /2/ + ] +qed. + +definition less_than_or_equal_b_elim: + ∀m, n: nat. + ∀P: bool → Type[0]. + (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n). + #m #n #P #H1 #H2; + lapply (less_than_or_equal_b_correct m n) + lapply (less_than_or_equal_b_complete m n) + cases (leb m n) + /3/ +qed. + +lemma inclusive_disjunction_true: + ∀b, c: bool. + (orb b c) = true → b = true ∨ c = true. + # b + # c + elim b + [ normalize + # H + @ or_introl + % + | normalize + /2/ + ] +qed. + +lemma conjunction_true: + ∀b, c: bool. + andb b c = true → b = true ∧ c = true. + # b + # c + elim b + normalize + [ /2/ + | # K + destruct + ] +qed. + +lemma eq_true_false: false=true → False. + # K + destruct +qed. + +lemma inclusive_disjunction_b_true: ∀b. orb b true = true. + # b + cases b + % +qed. + +definition bool_to_Prop ≝ + λb. match b with [ true ⇒ True | false ⇒ False ]. + +coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. + +lemma eq_false_to_notb: ∀b. b = false → ¬ b. + *; /2/ +qed. + +lemma length_append: + ∀A.∀l1,l2:list A. + |l1 @ l2| = |l1| + |l2|. + #A #l1 elim l1 + [ // + | #hd #tl #IH #l2 normalize ih ]="" qed.=""/ih/cons_prf/prfcr/refl_prf/cons_prf/prfcr/nil_prf/prfcr \ No newline at end of file diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma index 494177cfc..0fd4eb588 100644 --- a/weblib/basics/types.ma +++ b/weblib/basics/types.ma @@ -56,4 +56,6 @@ inductive option (A:Type[0]) : Type[0] ≝ (* sigma *) inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ - dp: ∀a:A.(f a)→Sig A f. \ No newline at end of file + dp: ∀a:A.(f a)→Sig A f. + +interpretation "Sigma" 'sigma x = (Sig ? x). diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index 80f49143a..c42e1887f 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -1,4 +1,3 @@ - include "tutorial/chapter2.ma". include "basics/bool.ma". diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 00b70a0da..cf7f4aafc 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -171,11 +171,11 @@ interpretation "in_prl mem" 'mem w l = (in_prl ? l w). interpretation "in_prl" 'in_l E = (in_prl ? E). lemma not_epsilon_lp :∀S.∀pi:a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S. a title="logical not" href="cic:/fakeuri.def(1)"¬/a ((a title="in_pl" href="cic:/fakeuri.def(1)"ℓ/a pi) a title="nil" href="cic:/fakeuri.def(1)"[/a]). -#S #pi (elim pi) normalize /2/ - [#pi1 #pi2 #H1 #H2 % * /2/ * #w1 * #w2 * * #appnil - cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil) /2/ - |#p11 #p12 #H1 #H2 % * /2/ - |#pi #H % * #w1 * #w2 * * #appnil (cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil)) /2/ +#S #pi (elim pi) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/ + [#pi1 #pi2 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ * #w1 * #w2 * * #appnil + cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#p11 #p12 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#pi #H % * #w1 * #w2 * * #appnil (cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ ] qed. @@ -183,7 +183,570 @@ lemma if_true_epsilon: ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def( #S #e #H %2 >H // qed. lemma if_epsilon_true : ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="nil" href="cic:/fakeuri.def(1)"[/a ] a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e → a title="snd" href="cic:/fakeuri.def(1)"\snd/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. -#S * #pi #b * [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/] cases b normalize // @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a +#S * #pi #b * [normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/] cases b normalize // @False_ind qed. - +definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉. + +notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. +interpretation "oplus" 'oplus a b = (lo ? a b). + +ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S. + match a with [ mk_pair e1 b1 ⇒ + match b1 with + [ false ⇒ 〈e1 · \fst b, \snd b〉 + | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]]. + +notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}. +interpretation "lc" 'lc op a b = (lc ? op a b). +notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}. + +ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S. + match a with [ mk_pair e1 b1 ⇒ + match b1 with + [ false ⇒ 〈e1^*, false〉 + | true ⇒ 〈(\fst (bcast ? e1))^*, true〉]]. + +notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}. +interpretation "lk" 'lk op a = (lk ? op a). +notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}. + +notation > "•" non associative with precedence 60 for @{eclose ?}. +nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝ + match E with + [ pz ⇒ 〈 ∅, false 〉 + | pe ⇒ 〈 ϵ, true 〉 + | ps x ⇒ 〈 `.x, false 〉 + | pp x ⇒ 〈 `.x, false 〉 + | po E1 E2 ⇒ •E1 ⊕ •E2 + | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉 + | pk E ⇒ 〈(\fst (•E))^*,true〉]. +notation < "• x" non associative with precedence 60 for @{'eclose $x}. +interpretation "eclose" 'eclose x = (eclose ? x). +notation > "• x" non associative with precedence 60 for @{'eclose $x}. + +ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉. +interpretation "reclose" 'eclose x = (reclose ? x). + +ndefinition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w. +notation > "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}. +notation "A =\sub 1 B" non associative with precedence 45 for @{'eq_f1 $A $B}. +interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b). + +naxiom extP : ∀S.∀p,q:word S → Prop.(p =1 q) → p = q. + +nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S] +#S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *; +nqed. + +nlemma cupA : ∀S.∀a,b,c:word S → Prop.a ∪ b ∪ c = a ∪ (b ∪ c). +#S a b c; napply extP; #w; nnormalize; @; *; /3/; *; /3/; nqed. + +nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a. +#S a b; napply extP; #w; @; *; nnormalize; /2/; nqed. + +(* theorem 16: 2 *) +nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2. +#S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2; +nwhd in ⊢ (??(??%)?); +nchange in ⊢(??%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2)); +nchange in ⊢(??(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2)); +nrewrite > (epsilon_or S …); nrewrite > (cupA S (𝐋\p e1) …); +nrewrite > (cupC ? (ϵ b1) …); nrewrite < (cupA S (𝐋\p e2) …); +nrewrite > (cupC ? ? (ϵ b1) …); nrewrite < (cupA …); //; +nqed. + +nlemma odotEt : + ∀S.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉. +#S e1 e2 b2; nnormalize; ncases (•e2); //; nqed. + +nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 |e2| ∪ 𝐋\p e2. //; nqed. + +nlemma cup_dotD : ∀S.∀p,q,r:word S → Prop.(p ∪ q) · r = (p · r) ∪ (q · r). +#S p q r; napply extP; #w; nnormalize; @; +##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj; +##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##] +nqed. + +nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p. +#S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed. + +nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 |e1 · e2| = 𝐋 |e1| · 𝐋 |e2|. +#S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj; +nqed. + +nlemma erase_plus : ∀S.∀e1,e2:pitem S.𝐋 |e1 + e2| = 𝐋 |e1| ∪ 𝐋 |e2|. +#S e1 e2; napply extP; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed. + +nlemma erase_star : ∀S.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed. + +ndefinition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w. +interpretation "substract" 'minus a b = (substract ? a b). + +nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}. +#S a b c; napply extP; #w; nnormalize; @; *; /4/; *; /4/; nqed. + +nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a. +#S a; napply extP; #w; nnormalize; @; /3/; *; //; nqed. + +nlemma subK : ∀S.∀a:word S → Prop. a - a = {}. +#S a; napply extP; #w; nnormalize; @; *; /2/; nqed. + +nlemma subW : ∀S.∀a,b:word S → Prop.∀w.(a - b) w → a w. +#S a b w; nnormalize; *; //; nqed. + +nlemma erase_bull : ∀S.∀a:pitem S. |\fst (•a)| = |a|. +#S a; nelim a; // by {}; +##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| · |e2|); + nrewrite < IH1; nrewrite < IH2; + nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊙ 〈e2,false〉)); + ncases (•e1); #e3 b; ncases b; nnormalize; + ##[ ncases (•e2); //; ##| nrewrite > IH2; //] +##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| + |e2|); + nrewrite < IH2; nrewrite < IH1; + nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊕ •e2)); + ncases (•e1); ncases (•e2); //; +##| #e IH; nchange in ⊢ (???%) with (|e|^* ); nrewrite < IH; + nchange in ⊢ (??(??%)?) with (\fst (•e))^*; //; ##] +nqed. + +nlemma eta_lp : ∀S.∀p:pre S.𝐋\p p = 𝐋\p 〈\fst p, \snd p〉. +#S p; ncases p; //; nqed. + +nlemma epsilon_dot: ∀S.∀p:word S → Prop. {[]} · p = p. +#S e; napply extP; #w; nnormalize; @; ##[##2: #Hw; @[]; @w; /3/; ##] +*; #w1; *; #w2; *; *; #defw defw1 Hw2; nrewrite < defw; nrewrite < defw1; +napply Hw2; nqed. + +(* theorem 16: 1 → 3 *) +nlemma odot_dot_aux : ∀S.∀e1,e2: pre S. + 𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 |\fst e2| → + 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2. +#S e1 e2 th1; ncases e1; #e1' b1'; ncases b1'; +##[ nwhd in ⊢ (??(??%)?); nletin e2' ≝ (\fst e2); nletin b2' ≝ (\snd e2); + nletin e2'' ≝ (\fst (•(\fst e2))); nletin b2'' ≝ (\snd (•(\fst e2))); + nchange in ⊢ (??%?) with (?∪?); + nchange in ⊢ (??(??%?)?) with (?∪?); + nchange in match (𝐋\p 〈?,?〉) with (?∪?); + nrewrite > (epsilon_or …); nrewrite > (cupC ? (ϵ ?)…); + nrewrite > (cupA …);nrewrite < (cupA ?? (ϵ?)…); + nrewrite > (?: 𝐋\p e2'' ∪ ϵ b2'' = 𝐋\p e2' ∪ 𝐋 |e2'|); ##[##2: + nchange with (𝐋\p 〈e2'',b2''〉 = 𝐋\p e2' ∪ 𝐋 |e2'|); + ngeneralize in match th1; + nrewrite > (eta_lp…); #th1; nrewrite > th1; //;##] + nrewrite > (eta_lp ? e2); + nchange in match (𝐋\p 〈\fst e2,?〉) with (𝐋\p e2'∪ ϵ b2'); + nrewrite > (cup_dotD …); nrewrite > (epsilon_dot…); + nrewrite > (cupC ? (𝐋\p e2')…); nrewrite > (cupA…);nrewrite > (cupA…); + nrewrite < (erase_bull S e2') in ⊢ (???(??%?)); //; +##| ncases e2; #e2' b2'; nchange in match (〈e1',false〉⊙?) with 〈?,?〉; + nchange in match (𝐋\p ?) with (?∪?); + nchange in match (𝐋\p (e1'·?)) with (?∪?); + nchange in match (𝐋\p 〈e1',?〉) with (?∪?); + nrewrite > (cup0…); + nrewrite > (cupA…); //;##] +nqed. + +nlemma sub_dot_star : + ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*. +#S X b; napply extP; #w; @; +##[ *; ##[##2: nnormalize; #defw; nrewrite < defw; @[]; @; //] + *; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj; + @ (w1 :: lw); nrewrite < defw; nrewrite < flx; @; //; + @; //; napply (subW … sube); +##| *; #wl; *; #defw Pwl; nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //] + #w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *; + ##[ *; #w1; *; #w2; *; *; #defwl' H1 H2; + @; ncases b in H1; #H1; + ##[##2: nrewrite > (sub0…); @w'; @(w1@w2); + nrewrite > (associative_append ? w' w1 w2); + nrewrite > defwl'; @; ##[@;//] @(wl'); @; //; + ##| ncases w' in Pw'; + ##[ #ne; @w1; @w2; nrewrite > defwl'; @; //; @; //; + ##| #x xs Px; @(x::xs); @(w1@w2); + nrewrite > (defwl'); @; ##[@; //; @; //; @; nnormalize; #; ndestruct] + @wl'; @; //; ##] ##] + ##| #wlnil; nchange in match (flatten ? (w'::wl')) with (w' @ flatten ? wl'); + nrewrite < (wlnil); nrewrite > (append_nil…); ncases b; + ##[ ncases w' in Pw'; /2/; #x xs Pxs; @; @(x::xs); @([]); + nrewrite > (append_nil…); @; ##[ @; //;@; //; nnormalize; @; #; ndestruct] + @[]; @; //; + ##| @; @w'; @[]; nrewrite > (append_nil…); @; ##[##2: @[]; @; //] + @; //; @; //; @; *;##]##]##] +nqed. + +(* theorem 16: 1 *) +alias symbol "pc" (instance 13) = "cat lang". +alias symbol "in_pl" (instance 23) = "in_pl". +alias symbol "in_pl" (instance 5) = "in_pl". +alias symbol "eclose" (instance 21) = "eclose". +ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|. +#S e; nelim e; //; + ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror; + ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *; + ##| #e1 e2 IH1 IH2; + nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉); + nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2); + nrewrite > (IH1 …); nrewrite > (cup_dotD …); + nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …); + nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …); + nrewrite < (erase_dot …); nrewrite < (cupA …); //; + ##| #e1 e2 IH1 IH2; + nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …); + nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …); + nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…); + nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …); + nrewrite < (erase_plus …); //. + ##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH; + nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉); + nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]}); + nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* ); + nrewrite > (erase_bull…e); + nrewrite > (erase_star …); + nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b')); ##[##2: + nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH; + ##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH; + nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//; + ##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##] + nrewrite > (cup_dotD…); nrewrite > (cupA…); + nrewrite > (?: ((?·?)∪{[]} = 𝐋 |e^*|)); //; + nchange in match (𝐋 |e^*|) with ((𝐋 |e|)^* ); napply sub_dot_star;##] + nqed. + +(* theorem 16: 3 *) +nlemma odot_dot: + ∀S.∀e1,e2: pre S. 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2. +#S e1 e2; napply odot_dot_aux; napply (bull_cup S (\fst e2)); nqed. + +nlemma dot_star_epsilon : ∀S.∀e:re S.𝐋 e · 𝐋 e^* ∪ {[]} = 𝐋 e^*. +#S e; napply extP; #w; nnormalize; @; +##[ *; ##[##2: #H; nrewrite < H; @[]; /3/] *; #w1; *; #w2; + *; *; #defw Hw1; *; #wl; *; #defw2 Hwl; @(w1 :: wl); + nrewrite < defw; nrewrite < defw2; @; //; @;//; +##| *; #wl; *; #defw Hwl; ncases wl in defw Hwl; ##[#defw; #; @2; nrewrite < defw; //] + #x xs defw; *; #Hx Hxs; @; @x; @(flatten ? xs); nrewrite < defw; + @; /2/; @xs; /2/;##] + nqed. + +nlemma nil_star : ∀S.∀e:re S. [ ] ∈ e^*. +#S e; @[]; /2/; nqed. + +nlemma cupID : ∀S.∀l:word S → Prop.l ∪ l = l. +#S l; napply extP; #w; @; ##[*]//; #; @; //; nqed. + +nlemma cup_star_nil : ∀S.∀l:word S → Prop. l^* ∪ {[]} = l^*. +#S a; napply extP; #w; @; ##[*; //; #H; nrewrite < H; @[]; @; //] #;@; //;nqed. + +nlemma rcanc_sing : ∀S.∀A,C:word S → Prop.∀b:word S . + ¬ (A b) → A ∪ { (b) } = C → A = C - { (b) }. +#S A C b nbA defC; nrewrite < defC; napply extP; #w; @; +##[ #Aw; /3/| *; *; //; #H nH; ncases nH; #abs; nlapply (abs H); *] +nqed. + +(* theorem 16: 4 *) +nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 |\fst e|)^*. +#S p; ncases p; #e b; ncases b; +##[ nchange in match (〈e,true〉^⊛) with 〈?,?〉; + nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); + nchange in ⊢ (??%?) with (?∪?); + nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* ); + nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b' )); ##[##2: + nlapply (bull_cup ? e); #bc; + nchange in match (𝐋\p (•e)) in bc with (?∪?); + nchange in match b' in bc with b'; + ncases b' in bc; ##[##2: nrewrite > (cup0…); nrewrite > (sub0…); //] + nrewrite > (cup_sub…); ##[napply rcanc_sing] //;##] + nrewrite > (cup_dotD…); nrewrite > (cupA…);nrewrite > (erase_bull…); + nrewrite > (sub_dot_star…); + nchange in match (𝐋\p 〈?,?〉) with (?∪?); + nrewrite > (cup_dotD…); nrewrite > (epsilon_dot…); //; +##| nwhd in match (〈e,false〉^⊛); nchange in match (𝐋\p 〈?,?〉) with (?∪?); + nrewrite > (cup0…); + nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 |e|^* ); + nrewrite < (cup0 ? (𝐋\p e)); //;##] +nqed. + +nlet rec pre_of_re (S : Alpha) (e : re S) on e : pitem S ≝ + match e with + [ z ⇒ pz ? + | e ⇒ pe ? + | s x ⇒ ps ? x + | c e1 e2 ⇒ pc ? (pre_of_re ? e1) (pre_of_re ? e2) + | o e1 e2 ⇒ po ? (pre_of_re ? e1) (pre_of_re ? e2) + | k e1 ⇒ pk ? (pre_of_re ? e1)]. + +nlemma notFalse : ¬False. @; //; nqed. + +nlemma dot0 : ∀S.∀A:word S → Prop. {} · A = {}. +#S A; nnormalize; napply extP; #w; @; ##[##2: *] +*; #w1; *; #w2; *; *; //; nqed. + +nlemma Lp_pre_of_re : ∀S.∀e:re S. 𝐋\p (pre_of_re ? e) = {}. +#S e; nelim e; ##[##1,2,3: //] +##[ #e1 e2 H1 H2; nchange in match (𝐋\p (pre_of_re S (e1 e2))) with (?∪?); + nrewrite > H1; nrewrite > H2; nrewrite > (dot0…); nrewrite > (cupID…);// +##| #e1 e2 H1 H2; nchange in match (𝐋\p (pre_of_re S (e1+e2))) with (?∪?); + nrewrite > H1; nrewrite > H2; nrewrite > (cupID…); // +##| #e1 H1; nchange in match (𝐋\p (pre_of_re S (e1^* ))) with (𝐋\p (pre_of_re ??) · ?); + nrewrite > H1; napply dot0; ##] +nqed. + +nlemma erase_pre_of_reK : ∀S.∀e. 𝐋 |pre_of_re S e| = 𝐋 e. +#S A; nelim A; //; +##[ #e1 e2 H1 H2; nchange in match (𝐋 (e1 · e2)) with (𝐋 e1·?); + nrewrite < H1; nrewrite < H2; // +##| #e1 e2 H1 H2; nchange in match (𝐋 (e1 + e2)) with (𝐋 e1 ∪ ?); + nrewrite < H1; nrewrite < H2; // +##| #e1 H1; nchange in match (𝐋 (e1^* )) with ((𝐋 e1)^* ); + nrewrite < H1; //] +nqed. + +(* corollary 17 *) +nlemma L_Lp_bull : ∀S.∀e:re S.𝐋 e = 𝐋\p (•pre_of_re ? e). +#S e; nrewrite > (bull_cup…); nrewrite > (Lp_pre_of_re…); +nrewrite > (cupC…); nrewrite > (cup0…); nrewrite > (erase_pre_of_reK…); //; +nqed. + +nlemma Pext : ∀S.∀f,g:word S → Prop. f = g → ∀w.f w → g w. +#S f g H; nrewrite > H; //; nqed. + +(* corollary 18 *) +ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ |e|. +#S e; @; +##[ #defsnde; nlapply (bull_cup ? e); nchange in match (𝐋\p (•e)) with (?∪?); + nrewrite > defsnde; #H; + nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //; + +STOP + +notation > "\move term 90 x term 90 E" +non associative with precedence 60 for @{move ? $x $E}. +nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ + match E with + [ pz ⇒ 〈 ∅, false 〉 + | pe ⇒ 〈 ϵ, false 〉 + | ps y ⇒ 〈 `y, false 〉 + | pp y ⇒ 〈 `y, x == y 〉 + | po e1 e2 ⇒ \move x e1 ⊕ \move x e2 + | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2 + | pk e ⇒ (\move x e)^⊛ ]. +notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}. +notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}. +interpretation "move" 'move x E = (move ? x E). + +ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e). +interpretation "rmove" 'move x E = (rmove ? x E). + +nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → False. +#S w abs; ninversion abs; #; ndestruct; +nqed. + + +nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False. +#S w abs; ninversion abs; #; ndestruct; +nqed. + +nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False. +#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe; +nqed. + + +naxiom in_move_cat: + ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) → + (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2. +#S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2); +ncases e1 in H; ncases e2; +##[##1: *; ##[*; nnormalize; #; ndestruct] + #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] + nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze; +##|##2: *; ##[*; nnormalize; #; ndestruct] + #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] + nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze; +##| #r; *; ##[ *; nnormalize; #; ndestruct] + #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] + ##[##2: nnormalize; #; ndestruct; @2; @2; //.##] + nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz; +##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##] + #H; ninversion H; nnormalize; #; ndestruct; + ##[ncases (?:False); /2/ by XXz] /3/ by or_intror; +##| #r1 r2; *; ##[ *; #defw] + ... +nqed. + +ntheorem move_ok: + ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E. +#S E; ncases E; #r b; nelim r; +##[##1,2: #a w; @; + ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##] + #H; ninversion H; #; ndestruct; + ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##] + #H; ninversion H; #; ndestruct;##] +##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##] + *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct; +##|#a c w; @; nnormalize; + ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2; nrewrite > (eqb_t … ca); @; ##] + #H; ninversion H; #; ndestruct; + ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct] + #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##] +##|#r1 r2 H1 H2 a w; @; + ##[ #H; ncases (in_move_cat … H); + ##[ *; #w1; *; #w2; *; *; #defw w1m w2m; + ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good; + nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //. + ##| + ... +##| +##| +##] +nqed. + + +notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}. +nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝ + match w with + [ nil ⇒ E + | cons x w' ⇒ w' ↦* (x ↦ \snd E)]. + +ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E). + +ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝ + mk_equiv: + ∀E1,E2: bool × (pre S). + \fst E1 = \fst E2 → + (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) → + equiv S E1 E2. + +ndefinition NAT: decidable. + @ nat eqb; /2/. +nqed. + +include "hints_declaration.ma". + +alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". +unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat. + +ninductive unit: Type[0] ≝ I: unit. + +nlet corec foo_nop (b: bool): + equiv ? + 〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉 + 〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?. + @; //; #x; ncases x + [ nnormalize in ⊢ (??%%); napply (foo_nop false) + | #y; ncases y + [ nnormalize in ⊢ (??%%); napply (foo_nop false) + | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##] +nqed. + +(* +nlet corec foo (a: unit): + equiv NAT + (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))))) + (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0))) +≝ ?. + @; + ##[ nnormalize; // + ##| #x; ncases x + [ nnormalize in ⊢ (??%%); + nnormalize in foo: (? → ??%%); + @; //; #y; ncases y + [ nnormalize in ⊢ (??%%); napply foo_nop + | #y; ncases y + [ nnormalize in ⊢ (??%%); + + ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##] + ##| #y; nnormalize in ⊢ (??%%); napply foo_nop + ##] +nqed. +*) + +ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0. +ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩. +ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*. + + +nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true. + nnormalize in match test3; + nnormalize; +//; +nqed. + +(**********************************************************) + +ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝ + der_z: der S a (z S) (z S) + | der_e: der S a (e S) (z S) + | der_s1: der S a (s S a) (e ?) + | der_s2: ∀b. a ≠ b → der S a (s S b) (z S) + | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' → + der S a (c ? e1 e2) (o ? (c ? e1' e2) e2') + | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' → + der S a (c ? e1 e2) (c ? e1' e2) + | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' → + der S a (o ? e1 e2) (o ? e1' e2'). + +nlemma eq_rect_CProp0_r: + ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p. + #A; #a; #x; #p; ncases p; #P; #H; nassumption. +nqed. + +nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed. + +naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2). +(* #S; #r1; #r2; #w; nelim r1 + [ #K; ninversion K + | #H1; #H2; napply (in_c ? []); // + | (* tutti casi assurdi *) *) + +ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝ + in_l_empty1: ∀E.in_l S [] E → in_l' S [] E + | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e. + +ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝ + mk_eq_re: ∀E1,E2. + (in_l S [] E1 → in_l S [] E2) → + (in_l S [] E2 → in_l S [] E1) → + (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') → + eq_re S E1 E2. + +(* serve il lemma dopo? *) +ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2. + #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ % + [ #r; #K (* ok *) + | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4; + +(* IL VICEVERSA NON VALE *) +naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E. +(* #S; #w; #E; #H; nelim H + [ // + | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *) + ] +nqed. *) + +ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e. + #S; #a; #E; #E'; #w; #H; nelim H + [##1,2: #H1; ninversion H1 + [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/ + |##2,9: #X; #Y; #K; ncases (?:False); /2/ + |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ + |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + |##6,13: #x; #y; #K; ncases (?:False); /2/ + |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/] +##| #H1; ninversion H1 + [ // + | #X; #Y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] +##| #H1; #H2; #H3; ninversion H3 + [ #_; #K; ncases (?:False); /2/ + | #X; #Y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] +##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6; \ No newline at end of file -- 2.39.2