From 5831a523c30368128dc7337835bc1e694b2ff095 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Apr 2007 14:29:38 +0000 Subject: [PATCH] ... --- matita/library/decidable_kit/decidable.ma | 197 ++++++++++++++++++++++ matita/library/decidable_kit/eqtype.ma | 170 +++++++++++++++++++ matita/library/decidable_kit/fintype.ma | 147 ++++++++++++++++ matita/library/decidable_kit/list_aux.ma | 123 ++++++++++++++ matita/library/decidable_kit/streicher.ma | 56 ++++++ 5 files changed, 693 insertions(+) create mode 100644 matita/library/decidable_kit/decidable.ma create mode 100644 matita/library/decidable_kit/eqtype.ma create mode 100644 matita/library/decidable_kit/fintype.ma create mode 100644 matita/library/decidable_kit/list_aux.ma create mode 100644 matita/library/decidable_kit/streicher.ma diff --git a/matita/library/decidable_kit/decidable.ma b/matita/library/decidable_kit/decidable.ma new file mode 100644 index 000000000..3aaa4a6ae --- /dev/null +++ b/matita/library/decidable_kit/decidable.ma @@ -0,0 +1,197 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/decidable_kit/decidable/". + +(* classical connectives for decidable properties *) + +include "decidable_kit/streicher.ma". +include "datatypes/bool.ma". +include "logic/connectives.ma". +include "nat/compare.ma". + +(* se non includi connectives accade un errore in modo reproducibile*) + +(* ### Prop <-> bool reflection predicate and lemmas for switching ### *) +inductive reflect (P : Prop) : bool → Type ≝ + | reflect_true : P → reflect P true + | reflect_false: ¬P → reflect P false. + +lemma b2pT : ∀P,b. reflect P b → b = true → P. +intros 3 (P b H); +(* XXX generalize in match H; clear H; rewrite > Db;*) +(* la rewrite pare non andare se non faccio la generalize *) +(* non va inversion: intros (H);inversion H; *) +cases H; [intros; assumption | intros 1 (ABS); destruct ABS ] +qed. + +lemma b2pF : ∀P,b. reflect P b → b = false → ¬P. +intros 3 (P b H); +cases H; [intros 1 (ABS); destruct ABS| intros; assumption] +qed. + +lemma p2bT : ∀P,b. reflect P b → P → b = true. +intros 4 (P b H Hp); +cases H (Ht Hf); [ intros; reflexivity | cases (Hf Hp)] +qed. + +lemma p2bF : ∀P,b. reflect P b → ¬P → b = false. +intros 4 (P b H Hp); +cases H (Ht Hf); [ cases (Hp Ht) | reflexivity ] +qed. + +lemma idP : ∀b:bool.reflect (b=true) b. +intros (b); cases b; [ constructor 1; reflexivity | constructor 2;] +unfold Not; intros (H); destruct H; +qed. + +(* ### standard connectives/relations with reflection predicate ### *) + +definition negb : bool → bool ≝ λb.match b with [ true ⇒ false | false ⇒ true]. + +lemma negbP : ∀b:bool.reflect (b = false) (negb b). +intros (b); cases b; simplify; [apply reflect_false | apply reflect_true] +[unfold Not; intros (H); destruct H | reflexivity] +qed. + +definition andb : bool → bool → bool ≝ + λa,b:bool. match a with [ true ⇒ b | false ⇒ false ]. + +lemma andbP : ∀a,b:bool. reflect (a = true ∧ b = true) (andb a b). +intros (a b); +generalize in match (refl_eq ? (andb a b)); +generalize in match (andb a b) in ⊢ (? ? ? % → %); intros 1 (c); +cases c; intros (H); [ apply reflect_true | apply reflect_false ]; +generalize in match H; clear H; +cases a; simplify; +[1: intros (E); rewrite > E; split; reflexivity +|2: intros (ABS); destruct ABS +|3: intros (E); rewrite > E; unfold Not; intros (ABS); decompose; destruct H1 +|4: intros (E); unfold Not; intros (ABS); decompose; destruct H] +qed. + +lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)). +intros (a b); cases a; cases b; simplify; +[1: apply reflect_false | *: apply reflect_true ] +[unfold Not; intros (H); cases H; destruct H1|right|left|left] reflexivity; +qed. + +definition orb : bool → bool → bool ≝ + λa,b.match a in bool with [true ⇒ true | false ⇒ b]. + +lemma orbP : ∀a,b:bool. reflect (a = true ∨ b = true) (orb a b). +intros (a b); cases a; cases b; simplify; +[1,2,3: apply reflect_true; [1,2: left | right ]; reflexivity +| apply reflect_false; unfold Not; intros (H); cases H (E E); destruct E] +qed. + +lemma orbC : ∀a,b. orb a b = orb b a. +intros (a b); cases a; cases b; auto. qed. + +lemma lebP: ∀x,y. reflect (x ≤ y) (leb x y). +intros (x y); generalize in match (leb_to_Prop x y); +cases (leb x y); simplify; intros (H); +[apply reflect_true | apply reflect_false ] assumption. +qed. + +lemma leb_refl : ∀n.leb n n = true. +intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed. + +lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true. +intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H; +apply (p2bT ? ? (lebP ? ?)); auto. +qed. + +definition ltb ≝ λx,y.leb (S x) y. + +lemma ltbP: ∀x,y. reflect (x < y) (ltb x y). +intros (x y); apply (lebP (S x) y); +qed. + +lemma ltb_refl : ∀n.ltb n n = false. +intros (n); apply (p2bF ? ? (ltbP ? ?)); auto; +qed. + +(* ### = between booleans as <-> in Prop ### *) +lemma eq_to_bool : + ∀a,b:bool. a = b → (a = true → b = true) ∧ (b = true → a = true). +intros (a b Eab); split; rewrite > Eab; intros; assumption; +qed. + +lemma bool_to_eq : + ∀a,b:bool. (a = true → b = true) ∧ (b = true → a = true) → a = b. +intros (a b Eab); decompose; +generalize in match H; generalize in match H1; clear H; clear H1; +cases a; cases b; intros (H1 H2); +[2: rewrite > (H2 ?) | 3: rewrite > (H1 ?)] reflexivity; +qed. + + +lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m. +intros (n m); apply bool_to_eq; split; intros (H); +[1:cases (b2pT ? ? (orbP ? ?) H); [2: auto] + rewrite > (eqb_true_to_eq ? ? H1); auto +|2:cases (b2pT ? ? (lebP ? ?) H); + [ elim n; [reflexivity|assumption] + | simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ] + reflexivity] +qed. + + +(* OUT OF PLACE *) +lemma ltW : ∀n,m. n < m → n < (S m). intros; auto. qed. + +lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true. +intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1; +apply (p2bT ? ? (ltbP ? ?) (ltW ? ? H1)); +qed. + +lemma ltS : ∀n,m.n < m → S n < S m. +intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H); +qed. + +lemma ltS' : ∀n,m.S n < S m → n < m. +intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H); +qed. + +lemma ltb_n_Sm : ∀m.∀n:nat. (orb (ltb n m) (eqb n m)) = ltb n (S m). +intros (m n); apply bool_to_eq; split; +[1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption] + rewrite > (eqb_true_to_eq ? ? H1); simplify; + rewrite > leb_refl; reflexivity +|2: generalize in match m; clear m; elim n 0; + [1: simplify; intros; cases n1; reflexivity; + |2: intros 1 (m); elim m 0; + [1: intros; apply (p2bT ? ? (orbP ? ?)); + lapply (H (pred n1) ?); [1: reflexivity] clear H; + generalize in match H1; + generalize in match Hletin; + cases n1; [1: simplify; intros; destruct H2] + intros; unfold pred in H; simplify in H; + cases (b2pT ? ? (orbP ? ?) H); [left|right] assumption; + |2: clear m; intros (m IH1 IH2 w); + lapply (IH1 ? (pred w)); + [3: generalize in match H; cases w; [2: intros; assumption] + simplify; intros; destruct H1; + |1: intros; apply (IH2 (S n1)); assumption; + |2: generalize in match H; generalize in match Hletin; + cases w; [1: simplify; intros; destruct H2] + intros (H H1); cases (b2pT ? ? (orbP ? ?) H); + apply (p2bT ? ? (orbP ? ?));[left|right] assumption]]]] +qed. + +(* non mi e' chiaro a cosa serva ... *) +lemma congr_S : ∀n,m.n = m → S n = S m. +intros 1; cases n; intros; rewrite > H; reflexivity. +qed. diff --git a/matita/library/decidable_kit/eqtype.ma b/matita/library/decidable_kit/eqtype.ma new file mode 100644 index 000000000..7b0f94ed4 --- /dev/null +++ b/matita/library/decidable_kit/eqtype.ma @@ -0,0 +1,170 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/decidable_kit/eqtype/". + +include "decidable_kit/decidable.ma". +include "datatypes/constructors.ma". + +(* ### types with a decidable AND rewrite (leibniz) compatible ### *) + +definition eq_compatible ≝ λT:Type.λa,b:T. reflect (a = b). + +record eqType : Type ≝ { + sort :> Type; + cmp : sort → sort → bool ; + eqP : ∀x,y:sort. eq_compatible sort x y (cmp x y) +}. + +lemma cmp_refl : ∀d:eqType.∀x. cmp d x x = true. +intros (d x); generalize in match (eqP d x x); intros (H); +unfold in H; (* inversion non fa whd!!! *) +inversion H; [ intros; reflexivity | intros (ABS); cases (ABS (refl_eq ? ?)) ] +qed. + +(* to use streicher *) +lemma eqType_decidable : ∀d:eqType. decT d. +intros (d); unfold decT; intros (x y); unfold decidable; +generalize in match (eqP d x y); intros (H); +cases H; [left | right] assumption; +qed. + +lemma eqbP : ∀x,y:nat. eq_compatible nat x y (eqb x y). +intros (x y); +generalize in match (refl_eq ? (eqb x y)); +generalize in match (eqb x y) in ⊢ (? ? ? % → %); intros 1 (b); +cases b; intros (H); [ apply reflect_true | apply reflect_false ]; +[ apply (eqb_true_to_eq ? ? H) | apply (eqb_false_to_not_eq ? ? H) ] +qed. + +definition nat_eqType : eqType ≝ mk_eqType ? ? eqbP. +(* XXX le coercion nel cast non vengono inserite *) +definition nat_canonical_eqType : nat → nat_eqType := + λn : nat.(n : sort nat_eqType). +coercion cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con. + +definition bcmp ≝ λx,y:bool. match x with [ true ⇒ y | false => notb y ]. + +lemma bcmpP : ∀x,y:bool. eq_compatible bool x y (bcmp x y). +intros (x y); +generalize in match (refl_eq ? (bcmp x y)); +generalize in match (bcmp x y) in ⊢ (? ? ? % → %); intros 1 (b); +cases b; intros (H); [ apply reflect_true | apply reflect_false ]; +generalize in match H; clear H; +cases x; cases y; simplify; intros (H); [1,4: reflexivity]; +(* non va: try destruct H; *) +[1,2,3,6: destruct H | *: unfold Not; intros (H1); destruct H1] +qed. + +definition bool_eqType : eqType ≝ mk_eqType ? ? bcmpP. +definition bool_canonical_eqType : bool → bool_eqType := + λb : bool.(b : sort bool_eqType). +coercion cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con. + +(* ### subtype of an eqType ### *) + +record sigma (d : eqType) (p : d -> bool) : Type ≝ { + sval : d; + sprop : p sval = true +}. + +notation "{x, h}" + right associative with precedence 80 +for @{'sig $x $h}. + +interpretation "sub_eqType" 'sig x h = + (cic:/matita/decidable_kit/eqtype/sigma.ind#xpointer(1/1/1) _ _ x h). + +(* restricting an eqType gives an eqType *) +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); + (* XXX destruct H; *) + change in Hcmp with (cmp d (match {?,ps} with [(mk_sigma s _)⇒s]) t = false); + rewrite > H in Hcmp; simplify in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp; +] +qed. + +definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p). + +inductive in_sub (d : eqType) (p : d → bool) (x : d) : option (sigma d p) → Type ≝ +| in_sig : ∀s : sigma d p. sval ? ? s = x → in_sub d p x (Some ? s) +| out_sig : p x = false → in_sub d p x (None ?). + +definition if_p ≝ λd:eqType.λp:d→bool.λx:d. + match (eqP bool_eqType (p x) true) with + [ (reflect_true H) ⇒ Some ? {?,H} + | (reflect_false _) ⇒ None ?]. + +lemma in_sub_eq : ∀d,p,x. in_sub d p x (if_p d p x). +intros (d p x); unfold if_p; +cases (eqP bool_eqType (p x) true); simplify; +[ apply in_sig; reflexivity; | apply out_sig; apply (p2bF ? ? (idP ?) H)] +qed. + +definition ocmp : ∀d:eqType.∀a,b:option d.bool ≝ + λd:eqType.λa,b:option d. + match a with + [ None ⇒ match b with [ None ⇒ true | (Some _) ⇒ false] + | (Some x) ⇒ match b with [ None ⇒ false | (Some y) ⇒ cmp d x y]]. + +lemma ocmpP : ∀d:eqType.∀a,b:option d.eq_compatible ? a b (ocmp d a b). +intros (d a b); +generalize in match (refl_eq ? (ocmp ? a b)); +generalize in match (ocmp ? a b) in ⊢ (? ? ? % → %); intros 1 (c); +cases c; intros (H); [ apply reflect_true | apply reflect_false ]; +generalize in match H; clear H; +cases a; cases b; +[1: intros; reflexivity; +|2,3: intros (H); destruct H; +|4: intros (H); simplify in H; rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; + (* se faccio la rewrite diretta non tipa *) +|5: intros (H H1); destruct H +|6,7: unfold Not; intros (H H1); destruct H1 +|8: unfold Not; simplify; intros (H H1); + (* ancora injection non va *) + cut (s = s1); [ rewrite > Hcut in H; rewrite > cmp_refl in H; destruct H;]. + change with (match (Some d s) with + [ None ⇒ s | (Some s) ⇒ s] = s1); rewrite > H1; + simplify; reflexivity; +] qed. + +definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d). +definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝ + λd:eqType.λx:d.(Some ? x : sort (option_eqType d)). +coercion cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con. + +(* belle le coercions! *) +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; +qed. diff --git a/matita/library/decidable_kit/fintype.ma b/matita/library/decidable_kit/fintype.ma new file mode 100644 index 000000000..c3e5ba41e --- /dev/null +++ b/matita/library/decidable_kit/fintype.ma @@ -0,0 +1,147 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/decidable_kit/fintype/". + +include "decidable_kit/eqtype.ma". +include "decidable_kit/list_aux.ma". + +record finType : Type ≝ { + fsort :> eqType; + enum : list fsort; + enum_uniq : ∀x:fsort. count fsort (cmp fsort x) enum = (S O) +}. + +definition segment : nat → eqType ≝ + λn.sub_eqType nat_eqType (λx:nat_eqType.ltb x n). + +definition is_some : ∀d:eqType. option d → bool ≝ + λd:eqType.λo:option d.notb (cmp (option_eqType d) (None ?) o). + +definition filter ≝ + λA,B:Type.λp:A→option B.λl:list A. + foldr A ? + (λx,acc. match (p x) with [None ⇒ acc | (Some y) ⇒ cons B y acc]) (nil B) l. + +definition segment_enum ≝ + λbound.filter ? ? (if_p nat_eqType (λx.ltb x bound)) (iota O bound). + +lemma iota_ltb : ∀x,p:nat. mem nat_eqType x (iota O p) = ltb x p. +intros (x p); elim p; simplify; [1:reflexivity] +rewrite < leb_eqb; +generalize in match (refl_eq ? (cmp ? x n)); +generalize in match (cmp ? x n) in ⊢ (? ? % ? → %); intros 1 (b); +cases b; simplify; intros (H1); [1: reflexivity] +rewrite > H; fold simplify (ltb x n); rewrite > H1; reflexivity; +qed. + +lemma mem_filter : + ∀d1,d2:eqType.(*∀y:d1.*)∀x:d2.∀l:list d1.∀p:d1 → option d2. + (∀y.mem d1 y l = true → + match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) → + mem d2 x (filter d1 d2 p l) = false. +intros 5 (d1 d2 x l p); +elim l; [1: simplify; auto] +simplify; fold simplify (filter d1 d2 p l1); +generalize in match (refl_eq ? (p t)); +generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; +[1: simplify; intros (Hpt); apply H; intros (y Hyl); + apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1)); + rewrite > Hyl; rewrite > orbC; reflexivity; +|2:simplify; intros (Hpt); + 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 < (H1 t); [2: simplify; rewrite > cmp_refl; reflexivity;] + rewrite > Hpt; simplify; symmetry; assumption; + |2: intros (Dxs); simplify; apply H; intros; + apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1)); + rewrite > H2; rewrite > orbC; reflexivity;]] +qed. + +lemma count_O : + ∀d:eqType.∀p:d→bool.∀l:list d. + (∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O. +intros 3 (d p l); elim l; simplify; [1: reflexivity] +fold simplify (count d p l1); (* XXX simplify troppo *) +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] auto. +|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; auto] + rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin] +qed. + +lemma segment_finType : nat → finType. +intros (bound); +letin fsort ≝ (segment bound); +letin enum ≝ (segment_enum bound); +cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O)); + [ apply (mk_finType fsort enum Hcut) + | intros (x); cases x (n Hn); simplify in Hn; clear x; + generalize in match Hn; generalize in match Hn; clear Hn; + unfold segment_enum; + generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?); + intros 1 (m); elim m (Hm Hn p IH Hm Hn); + [ destruct Hm; + | simplify; cases (eqP bool_eqType (ltb p bound) true); simplify; + (* XXX simplify che spacca troppo *) + fold simplify (filter nat_eqType (sigma nat_eqType (λx.ltb x bound)) + (if_p nat_eqType (λx.ltb x bound)) (iota O p)); + [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?); + unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?); + simplify in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?); + generalize in match (refl_eq ? (eqb n p)); + generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b); + cases b; simplify; + [2:intros (Enp); rewrite > IH; [1,3: auto] + rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm; + generalize in match Hm; cases (ltb n p); intros; [1:reflexivity] + simplify in H1; destruct H1; + |1:clear IH; intros (Enp); + fold simplify (count fsort (cmp fsort {n, Hn}) + (filter ? (sigma nat_eqType (λx.ltb x bound)) + (if_p nat_eqType (λx.ltb x bound)) (iota O p))); + rewrite > (count_O fsort); [1: 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: auto] + rewrite < ABS; symmetry; clear ABS; + generalize in match Hy; clear Hy; rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny); + simplify; intros (Hn); fold simplify (iota O n); + apply (mem_filter nat_eqType fsort); + intros (w Hw); + fold simplify (sort nat_eqType); + cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w); + simplify; [2: reflexivity] + generalize in match H1; clear H1; cases s; clear s; intros (H1); + unfold segment; simplify; simplify in H1; rewrite > H1; + rewrite > iota_ltb in Hw; + apply (p2bF ? ? (eqP nat_eqType ? ?)); + unfold Not; intros (Enw); + rewrite > Enw in Hw; rewrite > ltb_refl in Hw; destruct Hw] + |2:rewrite > IH; [1:reflexivity|3:assumption] + rewrite < ltb_n_Sm in Hm; + cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption] + rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn; + rewrite > Hn in H; cases (H ?); reflexivity; + ]]] +qed. diff --git a/matita/library/decidable_kit/list_aux.ma b/matita/library/decidable_kit/list_aux.ma new file mode 100644 index 000000000..8f30d3f6f --- /dev/null +++ b/matita/library/decidable_kit/list_aux.ma @@ -0,0 +1,123 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/decidable_kit/list_aux/". + +include "list/list.ma". +include "decidable_kit/eqtype.ma". +include "nat/plus.ma". + +(* ### some functions on lists (some can be moved to list.ma ### *) + +let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := + match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)]. + +definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l. + +definition count : ∀T : eqType.∀f : T → bool.∀l : list T. nat := + λT:eqType.λf,l. + foldr T nat (λx,acc. match (f x) with [ true ⇒ S acc | false ⇒ acc ]) O l. + +let rec mem (d : eqType) (x : d) (l : list d) on l : bool ≝ + match l with + [ nil ⇒ false + | cons y tl ⇒ + match (cmp d x y) with [ true ⇒ true | false ⇒ mem d x tl]]. + +definition iota : nat → nat → list nat ≝ + λn,m. nat_rect (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m. + +let rec map (A,B:Type) (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)]. + +(* ### induction principle for functions visiting 2 lists in parallel *) +lemma list_ind2 : + ∀T1,T2:Type.∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop. + length ? l1 = length ? l2 → + (P (nil ?) (nil ?)) → + (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → + P l1 l2. +intros (T1 T2 l1 l2 P Hl Pnil Pcons); +generalize in match Hl; clear Hl; +generalize in match l2; clear l2; +elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| destruct Hl] +| intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] + intros 1 (Hl); apply Pcons; + apply IH; destruct Hl; + (* XXX simplify in Hl non folda length *) + assumption;] +qed. + + +lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. +intros (A B f g l Efg); elim l; simplify; [1: reflexivity ]; +rewrite > (Efg t); rewrite > H; reflexivity; +qed. + +(* ### eqtype for lists ### *) +let rec lcmp (d : eqType) (l1,l2 : list d) on l1 : bool ≝ + match l1 with + [ nil ⇒ match l2 with [ nil ⇒ true | (cons _ _) ⇒ false] + | (cons x1 tl1) ⇒ match l2 with + [ nil ⇒ false | (cons x2 tl2) ⇒ andb (cmp d x1 x2) (lcmp d tl1 tl2)]]. + +lemma lcmp_length : + ∀d:eqType.∀l1,l2:list d. + lcmp ? l1 l2 = true → length ? l1 = length ? l2. +intros 2 (d l1); elim l1 1 (l2 x1); +[ cases l2; simplify; intros;[reflexivity|destruct H] +| intros 3 (tl1 IH l2); cases (l2); intros; [1:destruct H] + simplify; (* XXX la apply non fa simplify? *) + apply congr_S; apply (IH l); + (* XXX qualcosa di enorme e' rotto! la regola di convertibilita?! *) + simplify in H; + letin H' ≝ (b2pT ? ? (andbP ? ?) H); decompose; assumption] +qed. + +lemma lcmpP : ∀d:eqType.∀l1,l2:list d. eq_compatible (list d) l1 l2 (lcmp d l1 l2). +intros (d l1 l2); +generalize in match (refl_eq ? (lcmp d l1 l2)); +generalize in match (lcmp d l1 l2) in ⊢ (? ? ? % → %); intros 1 (c); +cases c; intros (H); [ apply reflect_true | apply reflect_false ] +[ letin Hl≝ (lcmp_length ? ? ? H); clearbody Hl; + generalize in match H; clear H; + apply (list_ind2 ? ? ? ? ? Hl); [1: intros; reflexivity] + simplify; intros (tl1 tl2 hd1 hd2 IH H); + letin H' ≝ (b2pT ? ? (andbP ? ?) H); decompose; + rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity +| generalize in match H; clear H; generalize in match l2; clear l2; + elim l1 1 (l1 x1); + [ cases l1; [intros; destruct H] + unfold Not; intros; destruct H1; + | intros 3 (tl1 IH l2); cases l2; + [ unfold Not; intros; destruct H1; + | simplify; intros; + letin H' ≝ (p2bT ? ? (negbP ?) H); clearbody H'; clear H; + letin H'' ≝ (b2pT ? ? (andbPF ? ?) H'); clearbody H''; clear H'; + cases H''; clear H''; + [ intros; + letin H' ≝ (b2pF ? ? (eqP d ? ?) H); clearbody H'; clear H; + (* XXX destruct H1; *) + change in H' with (Not ((match (x1::tl1) with [nil⇒x1|(cons x1 _) ⇒ x1]) = s)); + rewrite > H1 in H'; simplify in H'; apply H'; reflexivity; + | intros; + letin H' ≝ (IH ? H); clearbody H'; + (* XXX destruct H1 *) + change in H' with (Not ((match (x1::tl1) with [nil⇒tl1|(cons _ l) ⇒ l]) = l)); + rewrite > H1 in H'; simplify in H'; apply H'; reflexivity; + ]]]] +qed. + +definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d). + diff --git a/matita/library/decidable_kit/streicher.ma b/matita/library/decidable_kit/streicher.ma new file mode 100644 index 000000000..83c6f6169 --- /dev/null +++ b/matita/library/decidable_kit/streicher.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/decidable_kit/streicher/". + +include "logic/connectives.ma". +include "logic/equality.ma". + +definition step ≝ λT:Type.λa,b,c:T.λH1:a=b.λH2:a=c. eq_ind T ? (λx.b = x) H1 ? H2. + +lemma stepH : ∀T:Type.∀a:T.∀H:a=a. step ? ? ? ? H H = refl_eq T a. +intros (T a H); cases H; reflexivity. +qed. + +definition decT ≝ λT:Type.∀x,y:T. decidable (x=y). + +lemma nu : ∀T:Type.∀a,b:T. decT T → ∀E:a=b. a=b. +intros (T a b decT E); cases (decT a b) (Ecanonical Abs); [ exact Ecanonical | cases (Abs E) ] +qed. + +lemma nu_k : ∀T:Type.∀a,b:T.∀E1,E2:a=b. ∀d : decT T. nu ? ? ? d E1 = nu ? ? ? d E2. +intros (T a b E1 E2 decT); unfold nu; +cases (decT a b); simplify; [ reflexivity | cases (H E1) ] +qed. + +definition nu_inv ≝ λT:Type.λa,b:T. λd: decT T.λE:a=b. + step ? ? ? ? (nu ? ? ? d (refl_eq ? a)) E. + +definition cancel ≝ λT:Type.λA,B:Type.λf.λg:A→B.∀x:A.f (g x) = x. + +(* non inferisce Prop?!??! *) +lemma cancel_nu_nu_inv : ∀T:Type.∀a,b:T.∀d: decT T. + cancel Prop (a=b) (a=b) (nu_inv ? a b d) (nu ? a b d). +intros (T a b); unfold cancel; intros (E); cases E; +unfold nu_inv; rewrite > stepH; reflexivity. +qed. + +theorem pirrel : ∀T:Type.∀a,b:T.∀E1,E2:a=b.∀d: decT T. E1 = E2. +intros (T a b E1 E2 decT); +rewrite < (cancel_nu_nu_inv ? ? ? decT); +rewrite < (cancel_nu_nu_inv ? ? ? decT) in ⊢ (? ? ? %); +rewrite > (nu_k ? ? ? E1 E2 decT). +reflexivity. +qed. + -- 2.39.2