From f050491f27aa5a3d0d151f7268a5ffbfbe7d69df Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 12 Dec 2011 20:17:23 +0000 Subject: [PATCH] Some integrations from CerCo. In particular: 1) notation for destructuring let-ins for pairs, triples, quadruples, etc. 2) if-then-else is now a notation for pattern matching on booleans --- matita/matita/lib/arithmetics/bigops.ma | 8 +- matita/matita/lib/arithmetics/nat.ma | 4 +- matita/matita/lib/arithmetics/primes.ma | 3 +- matita/matita/lib/basics/bool.ma | 15 ++- matita/matita/lib/basics/lists/list.ma | 7 +- matita/matita/lib/basics/lists/listb.ma | 2 +- matita/matita/lib/basics/types.ma | 127 +++++++++++++++++++++--- 7 files changed, 135 insertions(+), 31 deletions(-) diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index 826c6a8b2..447cda347 100644 --- a/matita/matita/lib/arithmetics/bigops.ma +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -99,7 +99,7 @@ qed. theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k → \big[op,nil]_{i < n | p i}(f i) - = \big[op,nil]_{i < k | if_then_else ? (leb n i) false (p i)}(f i). + = \big[op,nil]_{i < k | if leb n i then false else p i}(f i). #k #n #p #B #nil #op #f #lenk (elim lenk) [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/ |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) // @@ -114,8 +114,8 @@ record Aop (A:Type[0]) (nil:A) : Type[0] ≝ theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B. op (\big[op,nil]_{inill @same_bigop #i #lti >(lt_to_leb_false … lti) normalize /2/ @@ -174,7 +174,7 @@ theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → [>bigop_Strue // >Hind >bigop_sum @same_bigop #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ #eqi [|#H] >eqi in ⊢ (???%); - >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize // + >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ #eqi >eqi in ⊢ (???%); >div_plus_times /2/ diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 56482a042..266f01ef8 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -700,10 +700,10 @@ theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false. (* min e max *) definition min: nat →nat →nat ≝ -λn.λm. if_then_else ? (leb n m) n m. +λn.λm. if leb n m then n else m. definition max: nat →nat →nat ≝ -λn.λm. if_then_else ? (leb n m) m n. +λn.λm. if leb n m then m else n. lemma commutative_min: commutative ? min. #n #m normalize @leb_elim diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma index c8b2a25bf..68e511e98 100644 --- a/matita/matita/lib/arithmetics/primes.ma +++ b/matita/matita/lib/arithmetics/primes.ma @@ -247,8 +247,7 @@ qed. (* smallest factor *) definition smallest_factor : nat → nat ≝ -λn:nat. if_then_else ? (leb n 1) n - (min n 2 (λm.(eqb (n \mod m) O))). +λn:nat. if leb n 1 then n else min n 2 (λm.(eqb (n \mod m) O)). theorem smallest_factor_to_min : ∀n. 1 < n → smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))). diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma index 7b2606485..7e874f412 100644 --- a/matita/matita/lib/basics/bool.ma +++ b/matita/matita/lib/basics/bool.ma @@ -76,11 +76,16 @@ lemma orb_true_l: ∀b1,b2:bool. (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true). * normalize /2/ qed. -definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝ -λA.λb.λ P,Q:A. match b with [ true ⇒ P | false ⇒ Q]. +definition xorb : bool → bool → bool ≝ +λb1,b2:bool. + match b1 with + [ true ⇒ match b2 with [ true ⇒ false | false ⇒ true ] + | false ⇒ match b2 with [ true ⇒ true | false ⇒ false ]]. -notation "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. -interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f). +notation > "'if' term 19 e 'then' term 19 t 'else' term 19 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] }. theorem bool_to_decidable_eq: ∀b1,b2:bool. decidable (b1=b2). @@ -109,4 +114,4 @@ record EnumSet : Type[1] ≝ { carr :> DeqSet; eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y) }. -*) \ No newline at end of file +*) diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index a1ffa3995..01766b9ec 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -95,7 +95,7 @@ let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝ definition filter ≝ λT.λp:T → bool. - foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T). + foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T). (* compose f [a1;...;an] [b1;...;bm] = [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *) @@ -150,8 +150,9 @@ qed. let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝ match l with [ nil ⇒ b - | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l)) - (fold A B op b p f l)]. + | cons a l ⇒ + if p a then op (f a) (fold A B op b p f l) + else fold A B op b p f l]. notation "\fold [ op , nil ]_{ ident i ∈ l | p} f" with precedence 80 diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma index 9af4b04a6..f5bf4df9e 100644 --- a/matita/matita/lib/basics/lists/listb.ma +++ b/matita/matita/lib/basics/lists/listb.ma @@ -105,7 +105,7 @@ let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝ [ nil ⇒ l2 | cons a tl ⇒ let r ≝ unique_append S tl l2 in - if (memb S a r) then r else a::r + if memb S a r then r else a::r ]. axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma index 2852662e4..0cf9aeadd 100644 --- a/matita/matita/lib/basics/types.ma +++ b/matita/matita/lib/basics/types.ma @@ -17,7 +17,26 @@ inductive void : Type[0] ≝. (* unit *) inductive unit : Type[0] ≝ it: unit. +(* sum *) +inductive Sum (A,B:Type[0]) : Type[0] ≝ + inl : A → Sum A B +| inr : B → Sum A B. + +interpretation "Disjoint union" 'plus A B = (Sum A B). + +(* option *) +inductive option (A:Type[0]) : Type[0] ≝ + None : option A + | Some : A → option A. + +(* sigma *) +inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ + dp: ∀a:A.(f a)→Sig A f. + +interpretation "Sigma" 'sigma x = (Sig ? x). + (* Prod *) + record Prod (A,B:Type[0]) : Type[0] ≝ { fst: A ; snd: B @@ -34,6 +53,19 @@ interpretation "pair pi2" 'pi2a x = (snd ? ? x). interpretation "pair pi1" 'pi1b x y = (fst ? ? x y). interpretation "pair pi2" 'pi2b x y = (snd ? ? x y). +notation "π1" with precedence 10 for @{ (proj1 ??) }. +notation "π2" with precedence 10 for @{ (proj2 ??) }. + +(* 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 = (mk_Prod ? ? (mk_Prod ? ? 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 = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)). + + theorem eq_pair_fst_snd: ∀A,B.∀p:A × B. p = 〈 \fst p, \snd p 〉. #A #B #p (cases p) // qed. @@ -44,20 +76,87 @@ lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a. lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b. // qed. -(* sum *) -inductive Sum (A,B:Type[0]) : Type[0] ≝ - inl : A → Sum A B -| inr : B → Sum A B. +notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" + with precedence 10 +for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }. -interpretation "Disjoint union" 'plus A B = (Sum A B). +notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp≝ break t \nbsp 'in' \nbsp) break s)" + with precedence 10 +for @{ match $t with [ mk_Prod (${ident x}:$X) (${ident y}:$Y) ⇒ $s ] }. -(* option *) -inductive option (A:Type[0]) : Type[0] ≝ - None : option A - | Some : A → option A. +(* Also extracts an equality proof (useful when not using Russell). *) +notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" + with precedence 10 +for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒ + λ${ident E}.$s ] (refl ? $t) }. -(* sigma *) -inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ - dp: ∀a:A.(f a)→Sig A f. - -interpretation "Sigma" 'sigma x = (Sig ? x). +notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)" + with precedence 10 +for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒ + λ${ident E}:$e.$s ] ($refl $T $t) }. + +notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" + with precedence 10 +for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒ + match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒ + λ${ident E}.$s ] ] (refl ? $t) }. + +notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)" + with precedence 10 +for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒ + match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒ + λ${ident E}:$J.$s ] ] ($refl $A $t) }. + +notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)" + with precedence 10 +for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${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 [ mk_Prod ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] ] }. + +(* This appears to upset automation (previously provable results require greater + depth or just don't work), so use example rather than lemma to prevent it + being indexed. *) +example contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e. +#A #B * // qed. + +lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. +((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → +∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. +#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. + +lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C. + R (P (\fst x) (\snd x)) → R (let 〈a,b〉 ≝ x in P a b). +#A #B #C *; normalize /2/ +qed. + +(* Is this necessary? +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). +*) + +(* Useful for avoiding destruct's full normalization. *) +lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2. +#A #B #a1 #a2 #b1 #b2 #H destruct // +qed. + +lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2. +#A #B #a1 #a2 #b1 #b2 #H destruct // +qed. + +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. \ No newline at end of file -- 2.39.2