From 441c4689edf514535218090c6ca70795d500b90a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 9 Sep 2007 19:00:57 +0000 Subject: [PATCH] ... --- matita/library/decidable_kit/eqtype.ma | 34 ++++---- matita/library/decidable_kit/fgraph.ma | 19 ++-- matita/library/decidable_kit/fintype.ma | 111 ++++++++---------------- 3 files changed, 60 insertions(+), 104 deletions(-) diff --git a/matita/library/decidable_kit/eqtype.ma b/matita/library/decidable_kit/eqtype.ma index ae0b07541..88721632f 100644 --- a/matita/library/decidable_kit/eqtype.ma +++ b/matita/library/decidable_kit/eqtype.ma @@ -90,20 +90,12 @@ interpretation "sub_eqType" 'sig x h = lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p. eq_compatible ? x y (cmp ? (sval ? ? x) (sval ? ?y)). intros (d p x y); -generalize in match (refl_eq ? (cmp d (sval d p x) (sval d p y))); -generalize in match (cmp d (sval d p x) (sval d p y)) in ⊢ (? ? ? % → %); intros 1 (b); -cases b; cases x (s ps); cases y (t pt); simplify; intros (Hcmp); -[ constructor 1; - generalize in match (eqP d s t); intros (Est); - cases Est (H); clear Est; - [ generalize in match ps; - rewrite > H; intros (pt'); - rewrite < (pirrel bool (p t) true pt pt' (eqType_decidable bool_eqType)); - reflexivity; - | cases (H (b2pT ? ? (eqP d s t) Hcmp)) - ] -| constructor 2; unfold Not; intros (H); destruct H; - rewrite > Hcut in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;] +cases (eqP d (sval ? ? x) (sval ? ? y)); generalize in match H; clear H; +cases x (s ps); cases y (t pt); simplify; intros (Est); +[1: constructor 1; generalize in match ps; rewrite > Est; intros (pt'); + rewrite < (pirrel ? ? ? pt pt' (eqType_decidable bool_eqType)); reflexivity; +|2: constructor 2; unfold Not; intros (H); destruct H; + cases (Est); assumption;] qed. definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p). @@ -153,9 +145,13 @@ coercion cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con. definition test_canonical_option_eqType ≝ (eq (option_eqType nat_eqType) O (S O)). -(* OUT OF PLACE *) -lemma eqbC : ∀x,y:nat. eqb x y = eqb y x. -intros (x y); apply bool_to_eq; split; intros (H); -rewrite > (b2pT ? ? (eqbP ? ?) H); rewrite > (cmp_refl nat_eqType); -reflexivity; +lemma cmpP : ∀d:eqType.∀x,y:d.∀P:bool → Prop. + (x=y → P true) → (cmp d x y = false → P false) → P (cmp d x y). +intros; cases (eqP ? x y); [2:apply H1; apply (p2bF ? ? (eqP d ? ?))] autobatch; +qed. + +lemma cmpC : ∀d:eqType.∀x,y:d. cmp d x y = cmp d y x. +intros; apply (cmpP ? x y); apply (cmpP ? y x); [1,4: intros; reflexivity] +[intros (H2 H1) | intros (H1 H2)] rewrite > H1 in H2; rewrite > cmp_refl in H2; +destruct H2. qed. diff --git a/matita/library/decidable_kit/fgraph.ma b/matita/library/decidable_kit/fgraph.ma index b2aca796b..a024ada3d 100644 --- a/matita/library/decidable_kit/fgraph.ma +++ b/matita/library/decidable_kit/fgraph.ma @@ -144,12 +144,9 @@ lemma mem_multes : intros (d e l s); elim l (hd tl IH); [cases s;simplify;[2: rewrite > andbC] reflexivity] simplify; rewrite > IH; cases s; simplify; [reflexivity] unfold list_eqType; simplify; -generalize in match (refl_eq ? (cmp d e s1)); generalize in match (cmp d e s1) in ⊢ (? ? ? % → %); -intros 1 (b); cases b; clear b; intros (E); cases (lcmp d l1 hd); -[1,2: rewrite > (b2pT ? ? (eqP ? ? ?) E); simplify; rewrite > cmp_refl; reflexivity -|3,4: rewrite > andbC; simplify; [2: reflexivity] rewrite > orbC; - simplify; apply (p2bF ? ? (eqP ? ? ?)); unfold Not; intros (H); rewrite > H in E; - rewrite > cmp_refl in E; destruct E;] +apply (cmpP ? e s1); cases (lcmp d l1 hd); intros (E); +[1,2: rewrite > E; simplify; rewrite > cmp_refl; reflexivity +|3,4: rewrite > cmpC; rewrite > E; simplify; reflexivity;] qed. lemma mem_concat: @@ -166,15 +163,13 @@ lemma mem_multss : match x in list with [ Nil ⇒ false | (Cons he tl) ⇒ andb (mem ? he s) (mem ? tl l)]. intros (d s l x); elim s; [cases x] simplify; try reflexivity; rewrite > mem_concat; rewrite > H; clear H; rewrite > mem_multes; cases x; simplify; [reflexivity] -unfold list_eqType; simplify; -generalize in match (refl_eq ? (cmp d t s1)); generalize in match (cmp d t s1) in ⊢ (? ? ? % → %); -intros 1 (b); cases b; clear b; intros (E); cases (mem d s1 l1); -[1,2: rewrite > (b2pT ? ? (eqP ? ? ?) E); rewrite > cmp_refl; simplify; +unfold list_eqType; simplify; apply (cmpP ? t s1); intros (E); +cases (mem d s1 l1); +[1,2: rewrite > E; rewrite > cmp_refl; simplify; [rewrite > orb_refl | rewrite > orbC ] reflexivity |3,4: simplify; rewrite > orbC; simplify; [reflexivity] symmetry; apply (p2bF ? ? (andbP ? ?)); unfold Not; intros (H); decompose; - rewrite > (b2pT ? ? (eqP ? ? ?) H1) in E; rewrite > cmp_refl in E; - destruct E] + rewrite > cmpC in H1; rewrite > E in H1; destruct H1;] qed. lemma mem_mkpermr_size : diff --git a/matita/library/decidable_kit/fintype.ma b/matita/library/decidable_kit/fintype.ma index 9b2dbadb9..ad71a4511 100644 --- a/matita/library/decidable_kit/fintype.ma +++ b/matita/library/decidable_kit/fintype.ma @@ -39,10 +39,9 @@ definition segment_enum ≝ lemma iota_ltb : ∀x,p:nat. mem nat_eqType x (iota O p) = ltb x p. intros (x p); elim p; simplify;[reflexivity] -generalize in match (refl_eq ? (cmp ? x n)); -generalize in match (cmp ? x n) in ⊢ (? ? ? % → %); intros 1 (b); -cases b; simplify; intros (H1); rewrite > H; clear H; -rewrite < (leb_eqb x n); rewrite > H1; reflexivity; +apply (cmpP nat_eqType x n); intros (E); rewrite > H; clear H; simplify; +[1: symmetry; apply (p2bT ? ? (lebP ? ?)); rewrite > E; apply le_n; +|2: rewrite < (leb_eqb x n); rewrite > E; reflexivity;] qed. lemma mem_filter : @@ -57,17 +56,11 @@ generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b [1: apply H; intros (y Hyl); apply H1; simplify; rewrite > Hyl; rewrite > orbC; reflexivity; -|2: generalize in match (refl_eq ? (cmp ? x s)); - generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - [1: simplify; intros (Exs); - rewrite > orbC; rewrite > H; - [2: intros; apply H1; simplify; rewrite > H2; rewrite > orbC; reflexivity - |1: lapply (H1 t) as H2; [2: simplify; rewrite > cmp_refl; reflexivity] - rewrite > Hpt in H2; simplify in H2; rewrite > H2 in Exs; - destruct Exs;] - |2: intros (Dxs); simplify; rewrite > H; - [2: intros; apply (H1 y); simplify; rewrite > H2; rewrite > orbC; reflexivity - |1: rewrite > Dxs; reflexivity]]] +|2: simplify; apply (cmpP d2 x s); simplify; intros (E); + [1: rewrite < (H1 t); simplify; [rewrite > Hpt; rewrite > E] + simplify; rewrite > cmp_refl; reflexivity + |2: apply H; intros; apply H1; simplify; rewrite > H2; + rewrite > orbC; reflexivity]] qed. lemma count_O : @@ -78,9 +71,7 @@ generalize in match (refl_eq ? (p t)); generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; simplify; [2:intros (Hpt); apply H; intros; apply H1; simplify; - generalize in match (refl_eq ? (cmp d x t)); - generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b1); - cases b1; simplify; intros; [2:rewrite > H2] autobatch. + apply (cmpP d x t); [2: rewrite > H2;]; intros; reflexivity; |1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch] rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin] qed. @@ -99,24 +90,16 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O)); simplify; cases (eqP bool_eqType (ltb p bound) true); simplify; [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?); unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?); - simplify; - generalize in match (refl_eq ? (eqb n p)); - generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b); cases b; clear b; - intros (Enp); simplify; + simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify; [2:rewrite > IH; [1,3: autobatch] rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm; - generalize in match Hm; cases (ltb n p); intros; [reflexivity] - simplify in H1; destruct H1; + rewrite > orbC in Hm; assumption; |1:clear IH; rewrite > (count_O fsort); [reflexivity] - intros 1 (x); rewrite < (b2pT ? ? (eqP ? n ?) Enp); - cases x (y Hy); intros (ABS); clear x; - unfold segment; unfold notb; simplify; - generalize in match (refl_eq ? (cmp ? n y)); - generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (Eny); simplify; [2:reflexivity] + intros 1 (x); rewrite < Enp; cases x (y Hy); + intros (ABS); clear x; unfold segment; unfold notb; simplify; + apply (cmpP ? n y); intros (Eny); simplify; [2:reflexivity] rewrite < ABS; symmetry; clear ABS; - generalize in match Hy; clear Hy; - rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny); + generalize in match Hy; clear Hy;rewrite < Eny; simplify; intros (Hn); apply (mem_filter nat_eqType fsort); intros (w Hw); fold simplify (sort nat_eqType); (* CANONICAL?! *) cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w); @@ -152,9 +135,7 @@ intros; cases a; cases b; reflexivity; qed. lemma uniq_tail : ∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l). intros (d x l); elim l; simplify; [reflexivity] -generalize in match (refl_eq ? (cmp d x t)); -generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; -intros (E); simplify ; rewrite > E; [reflexivity] +apply (cmpP d x t); intros (E); simplify ; rewrite > E; [reflexivity] rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA; rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity; qed. @@ -169,25 +150,20 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H] [1: generalize in match H2; simplify in H2; lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2; cases H3; clear H3; intros; - [2: lapply (uniq_mem ? ? ? H1) as H4; - generalize in match (refl_eq ? (cmp d x t)); - generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (H5); - [1: simplify; rewrite > H5; simplify; rewrite > count_O; [reflexivity] - intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H5) in H2 H3 H4 ⊢ %; - clear H5; clear x; rewrite > H2 in H4; destruct H4; + [2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t); + intros (H5); simplify; + [1: rewrite > count_O; [reflexivity] + intros (y Hy); rewrite > H5 in H2 H3 H4 ⊢ %; clear H5; clear x; + rewrite > H2 in H4; destruct H4; |2: simplify; rewrite > H5; simplify; apply H; rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption;] |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity] intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %; clear H2; clear x; lapply (uniq_mem ? ? ? H1) as H4; - generalize in match (refl_eq ? (cmp d t y)); - generalize in match (cmp d t y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (E); - [1: rewrite > (b2pT ? ? (eqP d ? ?) E) in H4; - rewrite > H4 in Hy; destruct Hy; - |2:intros; reflexivity]] -|2: rewrite > uniq_tail in H1; + apply (cmpP d t y); intros (E); [2: reflexivity]. + rewrite > E in H4; rewrite > H4 in Hy; destruct Hy;] +|2: rewrite > uniq_tail in H1; generalize in match (refl_eq ? (uniq d l1)); generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; [1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1; @@ -198,14 +174,11 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H] |2: simplify; rewrite > cmp_refl; reflexivity;] |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin; intros (r Mrl1); lapply (A r); - [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity] - generalize in match (refl_eq ? (cmp d r t)); - generalize in match (cmp d r t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - [1: intros (E); simplify in Hletin1; rewrite > E in Hletin1; - destruct Hletin1; rewrite < count_O_mem in Mrl1; - rewrite > Hcut in Mrl1; destruct Mrl1; - |2: intros; simplify in Hletin1; rewrite > H2 in Hletin1; - simplify in Hletin1; apply (Hletin1);]]] + [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity] + generalize in match Hletin1; simplify; apply (cmpP d r t); + simplify; intros (E Hc); [2: assumption] + destruct Hc; rewrite < count_O_mem in Mrl1; + rewrite > Hcut in Mrl1; destruct Mrl1;]] qed. lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true. @@ -228,36 +201,28 @@ cases (in_sub_eq d p t1); simplify; simplify; intros (Ert1); generalize in match Hr; clear Hr; rewrite > Ert1; clear Ert1; clear r; intros (Ht1); unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?); - simplify; generalize in match (refl_eq ? (cmp d t t1)); - generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (Ett1); simplify; + simplify; apply (cmpP ? t t1); simplify; intros (Ett1); [1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht}) (filter d (sigma d p) (if_p d p) l) = O); [1:rewrite > Hcut; reflexivity] lapply (uniq_mem ? ? ? H1); generalize in match Ht; - rewrite > (b2pT ? ? (eqP d ? ?) Ett1); intros (Ht1'); clear Ht1; + rewrite > Ett1; intros (Ht1'); clear Ht1; generalize in match Hletin; elim l; [ reflexivity] simplify; cases (in_sub_eq d p t2); simplify; [1: generalize in match H5; cases s; simplify; intros; clear H5; unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?); simplify; rewrite > H7; simplify in H4; - generalize in match H4; clear H4; - generalize in match (refl_eq ? (cmp d t1 t2)); - generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - simplify; intros; [1: destruct H5] apply H3; assumption; + generalize in match H4; clear H4; apply (cmpP ? t1 t2); + simplify; intros; [destruct H5] apply H3; assumption; |2: apply H3; - generalize in match H4; clear H4; simplify; - generalize in match (refl_eq ? (cmp d t1 t2)); - generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - simplify; intros; [1: destruct H6] assumption;] + generalize in match H4; clear H4; simplify; apply (cmpP ? t1 t2); + simplify; intros; [destruct H6] assumption;] |2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption] simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption] |2:rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption] - simplify in H2; generalize in match H2; generalize in match (refl_eq ? (cmp d t t1)); - generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (E); [2:assumption] - lapply (b2pT ? ? (eqP d ? ?) E); clear H; rewrite > Hletin in Ht; - rewrite > Ht in H3; destruct H3;] + simplify in H2; generalize in match H2; apply (cmpP ? t t1); + intros (E) [2:assumption] clear H; rewrite > E in Ht; rewrite > H3 in Ht; + destruct Ht;] qed. definition sub_finType : ∀d:finType.∀p:d→bool.finType ≝ -- 2.39.2