From b8a719bbb47d12e0a6b2c8cb2e5e26a2bf360be1 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 15 Nov 2011 14:11:45 +0000 Subject: [PATCH] commit by user andrea --- weblib/Cerco/ASM/JMCoercions.ma | 12 +- weblib/Cerco/ASM/Utils.ma | 493 +++++++++++++---------------- weblib/Cerco/utilities/pair.ma | 45 +++ weblib/Cerco/utilities/pair.ma.mad | 45 +++ weblib/basics/list.ma | 97 +++--- weblib/basics/list2.ma | 13 +- weblib/tutorial/chapter3.ma | 9 +- 7 files changed, 370 insertions(+), 344 deletions(-) create mode 100644 weblib/Cerco/utilities/pair.ma create mode 100644 weblib/Cerco/utilities/pair.ma.mad diff --git a/weblib/Cerco/ASM/JMCoercions.ma b/weblib/Cerco/ASM/JMCoercions.ma index 3f43e6b70..f36d310c0 100644 --- a/weblib/Cerco/ASM/JMCoercions.ma +++ b/weblib/Cerco/ASM/JMCoercions.ma @@ -2,11 +2,11 @@ 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]. +definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.a title="Sigma" href="cic:/fakeuri.def(1)"Σ/ax:A.P x ≝ λA,P,a,p. a href="cic:/matita/basics/types/Sig.con(0,1,2)"dp/a … a p. +definition eject : ∀A.∀P: A → Prop.(a title="Sigma" href="cic:/fakeuri.def(1)"Σ/ax: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 ?. +(* 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. @@ -16,8 +16,8 @@ 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). +lemma sig2: ∀A.∀P:A → Prop. ∀p:a title="Sigma" href="cic:/fakeuri.def(1)"Σ/ax:A.P x. P (a href="cic:/matita/Cerco/ASM/JMCoercions/eject.def(1)"eject/a … p). #A #P #p cases p #w #q @q qed. -(* END RUSSELL **) +(* END RUSSELL **) \ No newline at end of file diff --git a/weblib/Cerco/ASM/Utils.ma b/weblib/Cerco/ASM/Utils.ma index a7eeaad70..bcb583a95 100644 --- a/weblib/Cerco/ASM/Utils.ma +++ b/weblib/Cerco/ASM/Utils.ma @@ -1,70 +1,70 @@ -include "basics/list.ma". +include "basics/list2.ma". include "basics/types.ma". include "arithmetics/nat.ma". -include "utilities/pair.ma". -include "ASM/JMCoercions.ma". +include "Cerco/utilities/pair.ma". +include "Cerco/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. +axiom IMPOSSIBLE: a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,1,0)"K1DAEMONXXX/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,2,0)"K2DAEMONXXX/a. +example daemon: a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. generalize in match a href="cic:/matita/Cerco/ASM/Utils/IMPOSSIBLE.dec"IMPOSSIBLE/a; #IMPOSSIBLE destruct(IMPOSSIBLE) qed. +example not_implemented: a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. cases a href="cic:/matita/Cerco/ASM/Utils/daemon.def(2)" title="null"daemon/a qed. notation "⊥" with precedence 90 for @{ match ? in False with [ ] }. definition ltb ≝ - λm, n: nat. - leb (S m) n. + λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) n. definition geb ≝ - λm, n: nat. - ltb n m. + λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"ltb/a n m. definition gtb ≝ - λm, n: nat. - ltb n m. + λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"ltb/a 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 ≝ +let rec eq_nat (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝ match n with - [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ] - | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ] + [ O ⇒ match m with [ O ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ] + | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ] ]. let rec forall - (A: Type[0]) (f: A → bool) (l: list A) + (A: Type[0]) (f: A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ match l with - [ nil ⇒ true - | cons hd tl ⇒ f hd ∧ forall A f tl + [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a + | cons hd tl ⇒ f hd a title="boolean and" href="cic:/fakeuri.def(1)"∧/a forall A f tl ]. let rec prefix - (A: Type[0]) (k: nat) (l: list A) + (A: Type[0]) (k: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ match l with - [ nil ⇒ [ ] + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons hd tl ⇒ match k with - [ O ⇒ [ ] - | S k' ⇒ hd :: prefix A k' tl + [ O ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] + | S k' ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: 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|) + (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C) (proof: a title="norm" href="cic:/fakeuri.def(1)"|/aleft| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/aright|) on left: A ≝ - match left return λx. |x| = |right| → A with + match left return λx. a title="norm" href="cic:/fakeuri.def(1)"|/ax| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/aright| → A with [ nil ⇒ λnil_prf. - match right return λx. |[ ]| = |x| → A with + match right return λx. a title="norm" href="cic:/fakeuri.def(1)"|/aa title="nil" href="cic:/fakeuri.def(1)"[/a ]| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → 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 + match right return λx. a title="norm" href="cic:/fakeuri.def(1)"|/ahda title="cons" href="cic:/fakeuri.def(1)":/a:tl| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → A with [ nil ⇒ λcons_nil_absrd. ? | cons hd' tl' ⇒ λcons_cons_prf. fold_left2 … f (f accu hd hd') tl tl' ? @@ -75,49 +75,43 @@ let rec fold_left2 | 2: normalize in cons_nil_absrd; destruct(cons_nil_absrd) | 3: normalize in cons_cons_prf; - @injective_S + @a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a assumption ] -qed. +qed. let rec remove_n_first_internal - (i: nat) (A: Type[0]) (l: list A) (n: nat) + (i: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (A: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on l ≝ match l with - [ nil ⇒ [ ] + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons hd tl ⇒ - match eq_nat i n with + match a href="cic:/matita/Cerco/ASM/Utils/eq_nat.fix(0,0,1)"eq_nat/a i n with [ true ⇒ l - | _ ⇒ remove_n_first_internal (S i) A tl n + | _ ⇒ remove_n_first_internal (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i) A tl n ] ]. definition remove_n_first ≝ λA: Type[0]. - λn: nat. - λl: list A. - remove_n_first_internal 0 A l n. + λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + a href="cic:/matita/Cerco/ASM/Utils/remove_n_first_internal.fix(0,2,2)"remove_n_first_internal/a a title="natural number" href="cic:/fakeuri.def(1)"0/a 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) + (A: Type[0]) (i: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (res: ?) (rem: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → A → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on rem ≝ match rem with [ nil ⇒ res | cons e tl ⇒ - match geb i m with + match a href="cic:/matita/Cerco/ASM/Utils/geb.def(3)"geb/a i m with [ true ⇒ res - | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f + | _ ⇒ foldi_from_until_internal A (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a 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. + λA,n,m,f,a,l. a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until_internal.fix(0,3,4)"foldi_from_until_internal/a A a title="natural number" href="cic:/fakeuri.def(1)"0/a a (a href="cic:/matita/Cerco/ASM/Utils/remove_n_first.def(3)"remove_n_first/a A n l) m f. definition foldi_from ≝ λA: Type[0]. @@ -125,7 +119,7 @@ definition foldi_from ≝ λf. λa. λl. - foldi_from_until A n (|l|) f a l. + a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"foldi_from_until/a A n (a title="norm" href="cic:/fakeuri.def(1)"|/al|) f a l. definition foldi_until ≝ λA: Type[0]. @@ -133,117 +127,117 @@ definition foldi_until ≝ λf. λa. λl. - foldi_from_until A 0 m f a l. + a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"foldi_from_until/a A a title="natural number" href="cic:/fakeuri.def(1)"0/a m f a l. definition foldi ≝ λA: Type[0]. λf. λa. λl. - foldi_from_until A 0 (|l|) f a l. + a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"foldi_from_until/a A a title="natural number" href="cic:/fakeuri.def(1)"0/a (a title="norm" href="cic:/fakeuri.def(1)"|/al|) f a l. definition hd_safe ≝ λA: Type[0]. - λl: list A. - λproof: 0 < |l|. - match l return λx. 0 < |x| → A with + λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + λproof: a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/al|. + match l return λx. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → A with [ nil ⇒ λnil_absrd. ? | cons hd tl ⇒ λcons_prf. hd ] proof. normalize in nil_absrd; - cases(not_le_Sn_O 0) + cases(a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a a title="natural number" href="cic:/fakeuri.def(1)"0/a) #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 + λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + λproof: a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/al|. + match l return λx. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A with [ nil ⇒ λnil_absrd. ? | cons hd tl ⇒ λcons_prf. tl ] proof. normalize in nil_absrd; - cases(not_le_Sn_O 0) + cases(a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a a title="natural number" href="cic:/fakeuri.def(1)"0/a) #HYP cases(HYP nil_absrd) qed. let rec split - (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|) + (A: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (index: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (proof: index a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/al|) on index ≝ - match index return λx. x ≤ |l| → (list A) × (list A) with - [ O ⇒ λzero_prf. 〈[], l〉 + match index return λx. x a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/al| → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) a title="Product" href="cic:/fakeuri.def(1)"×/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) with + [ O ⇒ λzero_prf. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a], l〉 | S index' ⇒ λsucc_prf. - match l return λx. S index' ≤ |x| → (list A) × (list A) with + match l return λx. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a index' a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/ax| → (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) a title="Product" href="cic:/fakeuri.def(1)"×/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) with [ nil ⇒ λnil_absrd. ? | cons hd tl ⇒ λcons_prf. let 〈l1, l2〉 ≝ split A tl index' ? in - 〈hd :: l1, l2〉 + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd a title="cons" href="cic:/fakeuri.def(1)":/a: l1, l2〉 ] succ_prf ] proof. [1: normalize in nil_absrd; - cases(not_le_Sn_O index') + cases(a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a index') #HYP cases(HYP nil_absrd) |2: normalize in cons_prf; - @le_S_S_to_le + @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a assumption ] qed. let rec nth_safe - (elt_type: Type[0]) (index: nat) (the_list: list elt_type) - (proof: index < | the_list |) + (elt_type: Type[0]) (index: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (the_list: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a elt_type) + (proof: index a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a the_list |) on index ≝ - match index return λs. s < | the_list | → elt_type with + match index return λs. s a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a the_list | → elt_type with [ O ⇒ - match the_list return λt. 0 < | t | → elt_type with + match the_list return λt. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a 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 + match the_list return λt. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a index' a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a 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) + cases (a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a a title="natural number" href="cic:/fakeuri.def(1)"0/a) #ABSURD elim (ABSURD nil_absurd) | normalize in nil_absurd; - cases (not_le_Sn_O (S index')) + cases (a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"not_le_Sn_O/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a index')) #ABSURD elim (ABSURD nil_absurd) | normalize in cons_proof - @le_S_S_to_le + @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a 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. + λthe_list: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a elt_type. + λproof : a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="norm" href="cic:/fakeuri.def(1)"|/a the_list |. + a href="cic:/matita/Cerco/ASM/Utils/nth_safe.fix(0,1,6)"nth_safe/a elt_type (a title="norm" href="cic:/fakeuri.def(1)"|/athe_list| a title="natural minus" href="cic:/fakeuri.def(1)"-/a a title="natural number" href="cic:/fakeuri.def(1)"1/a) the_list ?. + normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_plus_to_minus.def(12)"lt_plus_to_minus/a/span/span/ +qed. let rec reduce - (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝ + (A: Type[0]) (B: Type[0]) (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on left ≝ match left with - [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 + [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], a title="nil" href="cic:/fakeuri.def(1)"[/a ]〉, a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], right〉〉 | cons hd tl ⇒ match right with - [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 + [ nil ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], left〉, a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="nil" href="cic:/fakeuri.def(1)"[/a ], a title="nil" href="cic:/fakeuri.def(1)"[/a ]〉〉 | 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〉〉 + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd a title="cons" href="cic:/fakeuri.def(1)":/a: commonl, restl〉, a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd' a title="cons" href="cic:/fakeuri.def(1)":/a: commonr, restr〉〉 ] ]. @@ -255,6 +249,7 @@ axiom reduce_strong: Σ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)| ≝ @@ -277,41 +272,41 @@ let rec reduce_strong >p2 >p3 >p4 normalize in ⊢ (% → ?) #HYP // ] -qed. +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 ≝ + (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on left ≝ match left with [ nil ⇒ match right with - [ nil ⇒ Some ? (nil C) - | _ ⇒ None ? + [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a C) + | _ ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? ] | cons hd tl ⇒ match right with - [ nil ⇒ None ? + [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? | cons hd' tl' ⇒ match map2_opt A B C f tl tl' with - [ None ⇒ None ? - | Some tail ⇒ Some ? (f hd hd' :: tail) + [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? + | Some tail ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (f hd hd' a title="cons" href="cic:/fakeuri.def(1)":/a: 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 + (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) (proof: a title="norm" href="cic:/fakeuri.def(1)"|/a left | a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/a right |) on left ≝ + match left return λx. a title="norm" href="cic:/fakeuri.def(1)"|/a x | a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/a right | → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C with [ nil ⇒ - match right return λy. | [] | = | y | → list C with - [ nil ⇒ λnil_prf. nil C + match right return λy. a title="norm" href="cic:/fakeuri.def(1)"|/a a title="nil" href="cic:/fakeuri.def(1)"[/a] | a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/a y | → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C with + [ nil ⇒ λnil_prf. a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a C | _ ⇒ λcons_absrd. ? ] | cons hd tl ⇒ - match right return λy. | hd::tl | = | y | → list C with + match right return λy. a title="norm" href="cic:/fakeuri.def(1)"|/a hda title="cons" href="cic:/fakeuri.def(1)":/a:tl | a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/a y | → a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a C with [ nil ⇒ λnil_absrd. ? - | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ? + | cons hd' tl' ⇒ λcons_prf. (f hd hd') a title="cons" href="cic:/fakeuri.def(1)":/a: map2 A B C f tl tl' ? ] ] proof. [1: normalize in cons_absrd; @@ -323,146 +318,86 @@ let rec map2 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 ≝ +let rec nub_by_internal (A: Type[0]) (f: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n ≝ match n with [ O ⇒ match l with - [ nil ⇒ [ ] + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons hd tl ⇒ l ] | S n ⇒ match l with - [ nil ⇒ [ ] + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons hd tl ⇒ - hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n + hd a title="cons" href="cic:/fakeuri.def(1)":/a: nub_by_internal A f (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? (λy. a href="cic:/matita/basics/bool/notb.def(1)"notb/a (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). + λf: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. + λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + a href="cic:/matita/Cerco/ASM/Utils/nub_by_internal.fix(0,3,3)"nub_by_internal/a A f l (a href="cic:/matita/basics/list2/length.fix(0,1,1)"length/a ? l). -let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝ +let rec member (A: Type[0]) (eq: A → A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (a: A) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ match l with - [ nil ⇒ false - | cons hd tl ⇒ orb (eq a hd) (member A eq a tl) + [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a + | cons hd tl ⇒ a href="cic:/matita/basics/bool/orb.def(1)"orb/a (eq a hd) (member A eq a tl) ]. -let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝ +let rec take (A: Type[0]) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on n: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A ≝ match n with - [ O ⇒ [ ] + [ O ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | S n ⇒ match l with - [ nil ⇒ [ ] - | cons hd tl ⇒ hd :: take A n tl + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] + | cons hd tl ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: take A n tl ] ]. -let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝ +let rec drop (A: Type[0]) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on n ≝ match n with [ O ⇒ l | S n ⇒ match l with - [ nil ⇒ [ ] + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | 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〉. + λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/Cerco/ASM/Utils/take.fix(0,1,1)"take/a A n l, a href="cic:/matita/Cerco/ASM/Utils/drop.fix(0,1,1)"drop/a 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 ≝ +let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → A → B) + (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝ match l with - [ nil ⇒ nil ? - | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl) + [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? + | cons hd tl ⇒ (f n hd) a title="cons" href="cic:/fakeuri.def(1)":/a: (mapi_internal A B (n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a title="natural number" href="cic:/fakeuri.def(1)"1/a) f tl) ]. definition mapi ≝ λA, B: Type[0]. - λf: nat → A → B. - λl: list A. - mapi_internal A B 0 f l. + λf: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → A → B. + λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. + a href="cic:/matita/Cerco/ASM/Utils/mapi_internal.fix(0,4,2)"mapi_internal/a A B a title="natural number" href="cic:/fakeuri.def(1)"0/a f l. let rec zip_pottier - (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) + (A: Type[0]) (B: Type[0]) (left: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (right: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on left ≝ match left with - [ nil ⇒ [ ] + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons hd tl ⇒ match right with - [ nil ⇒ [ ] - | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl' + [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] + | cons hd' tl' ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd, hd'〉 a title="cons" href="cic:/fakeuri.def(1)":/a: 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 ≝ @@ -486,23 +421,23 @@ let rec zip_safe @injective_S assumption ] -qed. +qed. *) -let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝ +let rec zip (A: Type[0]) (B: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (r: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on l: a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (A a title="Product" href="cic:/fakeuri.def(1)"×/a B)) ≝ match l with - [ nil ⇒ Some ? (nil (A × B)) + [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a (A a title="Product" href="cic:/fakeuri.def(1)"×/a B)) | cons hd tl ⇒ match r with - [ nil ⇒ None ? + [ nil ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? | cons hd' tl' ⇒ match zip ? ? tl tl' with - [ None ⇒ None ? - | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail) + [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? + | Some tail ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ahd, hd'〉 a title="cons" href="cic:/fakeuri.def(1)":/a: tail) ] ] ]. -let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝ +let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B) on l ≝ match l with [ nil ⇒ a | cons hd tl ⇒ foldl A B f (f a hd) tl @@ -513,9 +448,9 @@ lemma foldl_step: ∀B: Type[0]. ∀H: A → B → A. ∀acc: A. - ∀pre: list B. + ∀pre: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B. ∀hd:B. - foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd). + a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H acc (prea title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/ahd]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (H (a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a 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 ] @@ -526,24 +461,25 @@ lemma foldl_append: ∀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). + ∀suff,pre: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B. + a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H acc (prea title="append" href="cic:/fakeuri.def(1)"@/asuff) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a A B H (a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"foldl/a 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])) ] + [ #pre >a href="cic:/matita/basics/list/append_nil.def(4)"append_nil/a % + | #hd #tl #IH #pre whd in ⊢ (???%) <(a href="cic:/matita/Cerco/ASM/Utils/foldl_step.def(2)"foldl_step/a … H ??) applyS (IH (prea title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/ahd])) ] qed. definition flatten ≝ λA: Type[0]. - λl: list (list A). - foldr ? ? (append ?) [ ] l. + λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A). + a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ? ? (a href="cic:/matita/basics/list/append.fix(0,1,1)"append/a ?) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l. -let rec rev (A: Type[0]) (l: list A) on l ≝ +let rec rev (A: Type[0]) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ match l with - [ nil ⇒ nil A - | cons hd tl ⇒ (rev A tl) @ [ hd ] + [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A + | cons hd tl ⇒ (rev A tl) a title="append" href="cic:/fakeuri.def(1)"@/a a title="cons" href="cic:/fakeuri.def(1)"[/a hd ] ]. +(* lemma append_length: ∀A: Type[0]. ∀l, r: list A. @@ -618,7 +554,7 @@ lemma nth_append_second: | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk ] ] -qed. +qed.*) notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 @@ -627,17 +563,17 @@ notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp 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 ≝ + (f: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → A → B → A) (x: A) (i: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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 + | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i) tl ]. -definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. +definition fold_left_i ≝ λA,B,f,x. a href="cic:/matita/Cerco/ASM/Utils/fold_left_i_aux.fix(0,5,1)"fold_left_i_aux/a A B f x a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. -notation "hvbox(t⌈o ↦ h⌉)" +(* notation "hvbox(t\lceil o \mapsto h\rceil )" with precedence 45 - for @{ match (? : $o=$h) with [ refl ⇒ $t ] }. + for @{ match (? : $o=$h) with [ refl \Rightarrow $t ] }. *) definition function_apply ≝ λA, B: Type[0]. @@ -650,8 +586,14 @@ notation "f break $ x" for @{ 'function_apply $f $x }. interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). + +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 ≝ +let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n ≝ match n with [ O ⇒ a | S o ⇒ f (iterate A f a o) @@ -682,8 +624,8 @@ 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: Aa title="Product" href="cic:/fakeuri.def(1)"×/aB → C → Prop. + (∀lft, rgt. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgt〉 → P a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgt〉 (T lft rgt)) → P p (let 〈lft, rgt〉 ≝ p in T lft rgt). axiom pair_elim'': @@ -691,32 +633,32 @@ axiom pair_elim'': ∀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: Aa title="Product" href="cic:/fakeuri.def(1)"×/aB → C → C' → Prop. + (∀lft, rgt. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgt〉 → P a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,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/ + ∀A,B.∀a:A.∀b:B.∀c. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a c → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a c. + #A #B #a #b *; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/trans_eq.def(4)"trans_eq/a/span/span/ qed. lemma pair_destruct_2: - ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c. - #A #B #a #b *; /2/ + ∀A,B.∀a:A.∀b:B.∀c. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a c → b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a c. + #A #B #a #b *; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/trans_eq.def(4)"trans_eq/a/span/span/ qed. -let rec exclusive_disjunction (b: bool) (c: bool) on b ≝ +let rec exclusive_disjunction (b: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (c: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) on b ≝ match b with [ true ⇒ match c with - [ false ⇒ true - | true ⇒ false + [ false ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a + | true ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ] | false ⇒ match c with - [ false ⇒ false - | true ⇒ true + [ false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a + | true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a ] ]. @@ -726,21 +668,21 @@ 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 +let rec division_aux (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (n : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (p: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) ≝ + match a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"ltb/a n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a p) with + [ true ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | false ⇒ match m with - [ O ⇒ O - | (S q) ⇒ S (division_aux q (n - (S p)) p) + [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a + | (S q) ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (division_aux q (n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a p)) p) ] ]. definition division ≝ - λm, n: nat. + λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. match n with - [ O ⇒ S m - | S o ⇒ division_aux m m o + [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m + | S o ⇒ a href="cic:/matita/Cerco/ASM/Utils/division_aux.fix(0,0,3)"division_aux/a m m o ]. notation "hvbox(n break ÷ m)" @@ -749,21 +691,21 @@ notation "hvbox(n break ÷ 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 +let rec modulus_aux (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (p: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) ≝ + match a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n p with [ true ⇒ n | false ⇒ match m with [ O ⇒ n - | S o ⇒ modulus_aux o (n - (S p)) p + | S o ⇒ modulus_aux o (n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a p)) p ] ]. definition modulus ≝ - λm, n: nat. + λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. match n with [ O ⇒ m - | S o ⇒ modulus_aux m m o + | S o ⇒ a href="cic:/matita/Cerco/ASM/Utils/modulus_aux.fix(0,0,2)"modulus_aux/a m m o ]. notation "hvbox(n break 'mod' m)" @@ -773,13 +715,13 @@ notation "hvbox(n break 'mod' m)" interpretation "Nat modulus" 'modulus m n = (modulus m n). definition divide_with_remainder ≝ - λm, n: nat. - pair ? ? (m ÷ n) (modulus m n). + λm, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + a href="cic:/matita/basics/types/Prod.con(0,1,2)"pair/a ? ? (m a title="Nat division" href="cic:/fakeuri.def(1)"÷/a n) (a href="cic:/matita/Cerco/ASM/Utils/modulus.def(3)"modulus/a m n). -let rec exponential (m: nat) (n: nat) on n ≝ +let rec exponential (m: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) on n ≝ match n with - [ O ⇒ S O - | S o ⇒ m * exponential m o + [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a + | S o ⇒ m a title="natural times" href="cic:/fakeuri.def(1)"*/a exponential m o ]. interpretation "Nat exponential" 'exp n m = (exponential n m). @@ -790,16 +732,16 @@ 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: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n). #m #n #H elim H - /2/ + /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. theorem less_than_or_equal_b_complete: - ∀m, n: nat. - leb m n = false → ¬(m ≤ n). + ∀m, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="logical not" href="cic:/fakeuri.def(1)"¬/a(m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n). #m; elim m; normalize @@ -809,15 +751,15 @@ theorem less_than_or_equal_b_complete: cases z normalize [ #H - /2/ - | /3/ + /span class="autotactic"2span class="autotrace" trace {}/span/span/ + | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"not_le_to_not_le_S_S/a/span/span/ ] ] qed. theorem less_than_or_equal_b_correct: - ∀m, n: nat. - leb m n = true → m ≤ n. + ∀m, n: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. #m elim m // @@ -826,72 +768,65 @@ theorem less_than_or_equal_b_correct: normalize [ #H destruct - | #n #H lapply (H1 … H) /2/ + | #n #H lapply (H1 … H) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_monotone.def(2)"less_than_or_equal_monotone/a/span/span/ ] 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: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + ∀P: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Type[0]. + (m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → (a title="logical not" href="cic:/fakeuri.def(1)"¬/a(m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n) → P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → P (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a 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/ + lapply (a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_correct.def(3)"less_than_or_equal_b_correct/a m n) + lapply (a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_complete.def(6)"less_than_or_equal_b_complete/a m n) + cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a m n) + /span class="autotactic"3span class="autotrace" trace {}/span/span/ qed. lemma inclusive_disjunction_true: - ∀b, c: bool. - (orb b c) = true → b = true ∨ c = true. + ∀b, c: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. + (a href="cic:/matita/basics/bool/orb.def(1)"orb/a b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a c a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. # b # c elim b [ normalize # H - @ or_introl + @ a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a % | normalize - /2/ + /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ ] qed. lemma conjunction_true: - ∀b, c: bool. - andb b c = true → b = true ∧ c = true. + ∀b, c: a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. + a href="cic:/matita/basics/bool/andb.def(1)"andb/a b c a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a c a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. # b # c elim b normalize - [ /2/ + [ /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ | # K destruct ] qed. -lemma eq_true_false: false=true → False. +lemma eq_true_false: a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. # K destruct qed. -lemma inclusive_disjunction_b_true: ∀b. orb b true = true. +lemma inclusive_disjunction_b_true: ∀b. a href="cic:/matita/basics/bool/orb.def(1)"orb/a b a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. # b cases b % qed. definition bool_to_Prop ≝ - λb. match b with [ true ⇒ True | false ⇒ False ]. + λb. match b with [ true ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | false ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ]. -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. +coercion bool_to_Prop: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. Prop ≝ a href="cic:/matita/Cerco/ASM/Utils/bool_to_Prop.def(1)"bool_to_Prop/a on _b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a to Type[0]. -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 +lemma eq_false_to_notb: ∀b. b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="boolean not" href="cic:/fakeuri.def(1)"¬/a b. + *; /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/True.con(0,1,0)"I/a/span/span/ +qed. \ No newline at end of file diff --git a/weblib/Cerco/utilities/pair.ma b/weblib/Cerco/utilities/pair.ma new file mode 100644 index 000000000..613adb7ab --- /dev/null +++ b/weblib/Cerco/utilities/pair.ma @@ -0,0 +1,45 @@ +include "basics/types.ma". + +notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" + with precedence 10 +for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. + +(* 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 [ pair ${ident x} ${ident y} ⇒ + λ${ident E}.$s ] (refl ? $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 [ pair ${fresh xy} ${ident z} ⇒ + match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒ + λ${ident E}.$s ] ] (refl ? $t) }. + +(* 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. + +notation "π1" with precedence 10 for @{ (proj1 ??) }. +notation "π2" with precedence 10 for @{ (proj2 ??) }. + +(* 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. diff --git a/weblib/Cerco/utilities/pair.ma.mad b/weblib/Cerco/utilities/pair.ma.mad new file mode 100644 index 000000000..ceb214310 --- /dev/null +++ b/weblib/Cerco/utilities/pair.ma.mad @@ -0,0 +1,45 @@ +include "basics/types.ma". + +notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" + with precedence 10 +for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. + +(* 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 [ pair ${ident x} ${ident y} ⇒ + λ${ident E}.$s ] (refl ? $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 [ pair ${fresh xy} ${ident z} ⇒ + match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒ + λ${ident E}.$s ] ] (refl ? $t) }. + +(* 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:AA title="Product" href="cic:/fakeuri.def(1)"×/AB. (let 〈a,b〉 ≝ e in A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa,b〉) A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A e. +#A #B * // qed. + +lemma extract_pair : ∀A,B,C,D. ∀u:AA title="Product" href="cic:/fakeuri.def(1)"×/AB. ∀Q:A → B → CA title="Product" href="cic:/fakeuri.def(1)"×/AD. ∀x,y. +((let 〈a,b〉 ≝ u in Q a b) A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Ax,y〉) → +A title="exists" href="cic:/fakeuri.def(1)"∃/Aa,b. A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa,b〉 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A u A title="logical and" href="cic:/fakeuri.def(1)"∧/A Q a b A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Ax,y〉. +#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A @E1 qed. + +lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C. + R (P (A title="pair pi1" href="cic:/fakeuri.def(1)"\fst/A x) (A title="pair pi2" href="cic:/fakeuri.def(1)"\snd/A x)) → R (let 〈a,b〉 ≝ x in P a b). +#A #B #C *; normalize /2/ +qed. + +notation "π1" with precedence 10 for @{ (proj1 ??) }. +notation "π2" with precedence 10 for @{ (proj2 ??) }. + +(* Useful for avoiding destruct's full normalization. *) +lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa1,b1〉 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa2,b2〉 → a1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A a2. +#A #B #a1 #a2 #b1 #b2 #H destruct // +qed. + +lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa1,b1〉 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A A title="Pair construction" href="cic:/fakeuri.def(1)"〈/Aa2,b2〉 → b1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b2. +#A #B #a1 #a2 #b1 #b2 #H destruct // +qed. diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma index 14f7aaaa7..7d0c2ba13 100644 --- a/weblib/basics/list.ma +++ b/weblib/basics/list.ma @@ -31,12 +31,12 @@ notation "hvbox(l1 break @ l2)" interpretation "nil" 'nil = (nil ?). interpretation "cons" 'cons hd tl = (cons ? hd tl). -definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝ - λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ]. +definition not_nil: ∀A:Type[0].list A → Prop ≝ + λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ]. theorem nil_cons: - ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/a:l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a]. - #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq // + ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. + #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq // qed. (* @@ -45,24 +45,24 @@ let rec id_list A (l: list A) on l := [ nil => [] | (cons hd tl) => hd :: id_list A tl ]. *) -let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ +let rec append A (l1: list A) l2 on l1 ≝ match l1 with [ nil ⇒ l2 - | cons hd tl ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: append A tl l2 ]. + | cons hd tl ⇒ hd :: append A tl l2 ]. -definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.λd:A. +definition hd ≝ λA.λl: list A.λd:A. match l with [ nil ⇒ d | cons a _ ⇒ a]. -definition tail ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. - match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒ tl]. +definition tail ≝ λA.λl: list A. + match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. interpretation "append" 'append l1 l2 = (append ? l1 l2). -theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l. +theorem append_nil: ∀A.∀l:list A.l @ [] = l. #A #l (elim l) normalize // qed. theorem associative_append: - ∀A.a href="cic:/matita/basics/relations/associative.def(1)"associative/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/list/append.fix(0,1,1)"append/a A). + ∀A.associative (list A) (append A). #A #l1 #l2 #l3 (elim l1) normalize // qed. (* deleterio per auto @@ -71,41 +71,41 @@ ntheorem cons_append_commute: a :: (l1 @ l2) = (a :: l1) @ l2. //; nqed. *) -theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])a title="append" href="cic:/fakeuri.def(1)"@/al1. -/2/ qed. +theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1. +/span class="autotactic"2span class="autotrace" trace trans_eq/span/span/ qed. -theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. - l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/a] → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2. +theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. + l1@l2=[] → P (nil A) (nil A) → P l1 l2. #A #l1 #l2 #P (cases l1) normalize // #a #l3 #heq destruct qed. -theorem nil_to_nil: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. - l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a]. -#A #l1 #l2 #isnil @(a href="cic:/matita/basics/list/nil_append_elim.def(3)"nil_append_elim/a A l1 l2) /2/ +theorem nil_to_nil: ∀A.∀l1,l2:list A. + l1@l2 = [] → l1 = [] ∧ l2 = []. +#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /span class="autotactic"2span class="autotrace" trace conj/span/span/ qed. (* iterators *) -let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝ - match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)]. +let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝ + match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. -let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝ +let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)]. definition filter ≝ - λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. - a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p x) (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T). + λT.λp:T → bool. + foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T). -lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → - a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l. +lemma filter_true : ∀A,l,a,p. p a = true → + filter A p (a::l) = a :: filter A p l. #A #l #a #p #pa (elim l) normalize >pa normalize // qed. -lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → - a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l. +lemma filter_false : ∀A,l,a,p. p a = false → + filter A p (a::l) = filter A p l. #A #l #a #p #pa (elim l) normalize >pa normalize // qed. -theorem eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l. +theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. #A #B #f #g #l #eqfg (elim l) normalize // qed. (* @@ -132,10 +132,10 @@ let rec nth n (A:Type[0]) (l:list A) (d:A) ≝ **************************** fold *******************************) -let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (f:A→B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝ +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 ⇒ a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p a) (op (f a) (fold A B op b p f l)) + | 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)]. notation "\fold [ op , nil ]_{ ident i ∈ l | p} f" @@ -149,38 +149,37 @@ for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}. interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l). theorem fold_true: -∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). +∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → + \fold[op,nil]_{i ∈ a::l| p i} (f i) = + op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). #A #B #a #l #p #op #nil #f #pa normalize >pa // qed. theorem fold_false: ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f. -p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). +p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = + \fold[op,nil]_{i ∈ l| p i} (f i). #A #B #a #l #p #op #nil #f #pa normalize >pa // qed. theorem fold_filter: ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B. - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)} (f i). + \fold[op,nil]_{i ∈ l| p i} (f i) = + \fold[op,nil]_{i ∈ (filter A p l)} (f i). #A #B #a #l #p #op #nil #f elim l // -#a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa - [ >a href="cic:/matita/basics/list/filter_true.def(3)"filter_true/a // > a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // >a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // - | >a href="cic:/matita/basics/list/filter_false.def(3)"filter_false/a // >a href="cic:/matita/basics/list/fold_false.def(3)"fold_false/a // ] +#a #tl #Hind cases(true_or_false (p a)) #pa + [ >filter_true // > fold_true // >fold_true // + | >filter_false // >fold_false // ] qed. record Aop (A:Type[0]) (nil:A) : Type[0] ≝ {op :2> A → A → A; - nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; - nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; - assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a op (op a b) c + nill:∀a. op nil a = a; + nilr:∀a. op a nil = a; + assoc: ∀a,b,c.op a (op b c) = op (op a b) c }. -theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f. - op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i). +theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f. + op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) = + \fold[op,nil]_{i∈(I@J)} (f i). #A #B #I #J #nil #op #f (elim I) normalize - [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //] -qed. - + [>nill //|#a #tl #Hind