From c5608d2704215a7004d23f4801e19df3939f0285 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Apr 2007 14:32:28 +0000 Subject: [PATCH] set -> type --- helm/software/matita/library/Fsub/defn.ma | 54 ++++++------- helm/software/matita/library/Fsub/part1a.ma | 2 +- helm/software/matita/library/Fsub/util.ma | 2 +- helm/software/matita/library/list/sort.ma | 26 +++---- helm/software/matita/tests/discriminate.ma | 85 ++++++++++++++++----- 5 files changed, 110 insertions(+), 59 deletions(-) diff --git a/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/library/Fsub/defn.ma index 8ff30ce1f..97e161967 100644 --- a/helm/software/matita/library/Fsub/defn.ma +++ b/helm/software/matita/library/Fsub/defn.ma @@ -21,7 +21,7 @@ include "list/list.ma". include "Fsub/util.ma". (*** representation of Fsub types ***) -inductive Typ : Set \def +inductive Typ : Type \def | TVar : nat \to Typ (* type var *) | TFree: nat \to Typ (* free type name *) | Top : Typ (* maximum type *) @@ -29,7 +29,7 @@ inductive Typ : Set \def | Forall : Typ \to Typ \to Typ. (* universal type *) (*** representation of Fsub terms ***) -inductive Term : Set \def +inductive Term : Type \def | Var : nat \to Term (* variable *) | Free : nat \to Term (* free name *) | Abs : Typ \to Term \to Term (* abstraction *) @@ -39,7 +39,7 @@ inductive Term : Set \def (* representation of bounds *) -record bound : Set \def { +record bound : Type \def { istype : bool; (* is subtyping bound? *) name : nat ; (* name *) btype : Typ (* type to which the name is bound *) @@ -354,11 +354,11 @@ lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to \exists B,T.(in_list ? (mk_bound B x T) G). intros 2;elim G 0 [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin - |intros 3;elim s;simplify in H1;inversion H1 + |intros 3;elim t;simplify in H1;inversion H1 [intros;rewrite < H2;simplify;apply ex_intro [apply b |apply ex_intro - [apply t + [apply t1 |lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin; apply in_Base]] |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2; @@ -411,7 +411,7 @@ lemma varin_envappend_case: \forall G,H,x.(var_in_env x (H @ G)) \to (var_in_env x G) \lor (var_in_env x H). intros 3.elim H 0 [simplify;intro;left;assumption - |intros 2;elim s;simplify in H2;inversion H2 + |intros 2;elim t;simplify in H2;inversion H2 [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;right; simplify;constructor 1 |intros;lapply (inj_tail ? ? ? ? ? H6); @@ -441,10 +441,10 @@ lemma varinG_or_varinH_to_varinGH : \forall G,H,x. intros.elim H1 0 [elim H [simplify;assumption - |elim s;simplify;constructor 2;apply (H2 H3)] + |elim t;simplify;constructor 2;apply (H2 H3)] |elim H 0 [simplify;intro;lapply (in_list_nil nat x H2);elim Hletin - |intros 2;elim s;simplify in H3;inversion H3 + |intros 2;elim t;simplify in H3;inversion H3 [intros;lapply (inj_head_nat ? ? ? ? H5);rewrite > Hletin;simplify; constructor 1 |intros;simplify;constructor 2;rewrite < H6;apply H2; @@ -481,7 +481,7 @@ lemma fv_env_extends : \forall H,x,B,C,T,U,G. (fv_env (H @ ((mk_bound C x U) :: G))). intros;elim H [simplify;reflexivity - |elim s;simplify;rewrite > H1;reflexivity] + |elim t;simplify;rewrite > H1;reflexivity] qed. lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. @@ -597,7 +597,7 @@ lemma lookup_swap : \forall x,u,v,T,B,G.(in_list ? (mk_bound B x T) G) \to (in_list ? (mk_bound B (swap u v x) (swap_Typ u v T)) (swap_Env u v G)). intros 6;elim G 0 [intros;elim (in_list_nil ? ? H) - |intro;elim s;simplify;inversion H1 + |intro;elim t;simplify;inversion H1 [intros;lapply (inj_head ? ? ? ? H3);rewrite < H2 in Hletin; destruct Hletin;rewrite > Hcut;rewrite > Hcut1;rewrite > Hcut2; apply in_Base @@ -628,13 +628,13 @@ lemma in_dom_swap : \forall u,v,x,G. intros;split [elim G 0 [simplify;intro;elim (in_list_nil ? ? H) - |intro;elim s 0;simplify;intros;inversion H1 + |intro;elim t 0;simplify;intros;inversion H1 [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2; rewrite > H4 in H;apply in_Skip;apply (H H2)]] |elim G 0 [simplify;intro;elim (in_list_nil ? ? H) - |intro;elim s 0;simplify;intros;inversion H1 + |intro;elim t 0;simplify;intros;inversion H1 [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite < H2 in Hletin; lapply (swap_inj ? ? ? ? Hletin);rewrite > Hletin1;apply in_Base |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2; @@ -657,7 +657,7 @@ cut (\forall l:(list nat).\exists n.\forall m. [assumption|apply nil_cons] |intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = []) [assumption|apply nil_cons]]] - |elim H;lapply (decidable_eq_nat a s);elim Hletin + |elim H;lapply (decidable_eq_nat a t);elim Hletin [apply ex_intro [apply (S a) |intros;unfold;intro;inversion H4 @@ -668,23 +668,23 @@ cut (\forall l:(list nat).\exists n.\forall m. rewrite < H7 in H5; apply (H1 m ? H5);lapply (le_S ? ? H3); apply (le_S_S_to_le ? ? Hletin2)]] - |cut ((leb a s) = true \lor (leb a s) = false) + |cut ((leb a t) = true \lor (leb a t) = false) [elim Hcut [apply ex_intro - [apply (S s) + [apply (S t) |intros;unfold;intro;inversion H5 [intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4; rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4) |intros;lapply (inj_tail ? ? ? ? ? H9); rewrite < Hletin1 in H6;lapply (H1 a1) [apply (Hletin2 H6) - |lapply (leb_to_Prop a s);rewrite > H3 in Hletin2; + |lapply (leb_to_Prop a t);rewrite > H3 in Hletin2; simplify in Hletin2;rewrite < H8; apply (trans_le ? ? ? Hletin2); apply (trans_le ? ? ? ? H4);constructor 2;constructor 1]]] |apply ex_intro [apply a - |intros;lapply (leb_to_Prop a s);rewrite > H3 in Hletin1; + |intros;lapply (leb_to_Prop a t);rewrite > H3 in Hletin1; simplify in Hletin1;lapply (not_le_to_lt ? ? Hletin1); unfold in Hletin2;unfold;intro;inversion H5 [intros;lapply (inj_head_nat ? ? ? ? H7); @@ -693,7 +693,7 @@ cut (\forall l:(list nat).\exists n.\forall m. |intros;lapply (inj_tail ? ? ? ? ? H9); rewrite < Hletin3 in H6;rewrite < H8 in H6; apply (H1 ? H4 H6)]]] - |elim (leb a s);auto]]]] + |elim (leb a t);auto]]]] qed. (*** lemmas on well-formedness ***) @@ -794,17 +794,17 @@ qed. lemma WFE_swap : \forall u,v,G.(WFEnv G) \to (WFEnv (swap_Env u v G)). intros 3.elim G 0 [intro;simplify;assumption - |intros 2;elim s;simplify;constructor 2 + |intros 2;elim t;simplify;constructor 2 [apply H;apply (WFE_consG_WFE_G ? ? H1) |unfold;intro;lapply (in_dom_swap u v n l);elim Hletin;lapply (H4 H2); (* FIXME trick *)generalize in match H1;intro;inversion H1 - [intros;absurd ((mk_bound b n t)::l = []) + [intros;absurd ((mk_bound b n t1)::l = []) [assumption|apply nil_cons] |intros;lapply (inj_head ? ? ? ? H10);lapply (inj_tail ? ? ? ? ? H10); destruct Hletin2;rewrite < Hcut1 in H8;rewrite < Hletin3 in H8; apply (H8 Hletin1)] - |apply (WFT_swap u v l t);inversion H1 - [intro;absurd ((mk_bound b n t)::l = []) + |apply (WFT_swap u v l t1);inversion H1 + [intro;absurd ((mk_bound b n t1)::l = []) [assumption|apply nil_cons] |intros;lapply (inj_head ? ? ? ? H6);lapply (inj_tail ? ? ? ? ? H6); destruct Hletin;rewrite > Hletin1;rewrite > Hcut2;assumption]]] @@ -929,11 +929,11 @@ lemma swap_env_not_free : \forall u,v,G.(WFEnv G) \to (swap_Env u v G) = G. intros 3.elim G 0 [simplify;intros;reflexivity - |intros 2;elim s 0;simplify;intros;lapply (notin_cons ? ? ? ? H2); + |intros 2;elim t 0;simplify;intros;lapply (notin_cons ? ? ? ? H2); lapply (notin_cons ? ? ? ? H3);elim Hletin;elim Hletin1; lapply (swap_other ? ? ? H4 H6);lapply (WFE_consG_to_WFT ? ? ? ? H1); - cut (\lnot (in_list ? u (fv_type t))) - [cut (\lnot (in_list ? v (fv_type t))) + cut (\lnot (in_list ? u (fv_type t1))) + [cut (\lnot (in_list ? v (fv_type t1))) [lapply (swap_Typ_not_free ? ? ? Hcut Hcut1); lapply (WFE_consG_WFE_G ? ? H1); lapply (H Hletin5 H5 H7); @@ -1123,9 +1123,9 @@ intros 7;elim H 0 |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8); destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4; rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)] - |intros;simplify;generalize in match H2;elim s;simplify in H4; + |intros;simplify;generalize in match H2;elim t;simplify in H4; inversion H4 - [intros;absurd (mk_bound b n t::l@(mk_bound B x T::G)=Empty) + [intros;absurd (mk_bound b n t1::l@(mk_bound B x T::G)=Empty) [assumption |apply nil_cons] |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9); diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma index e12a64be4..795546299 100644 --- a/helm/software/matita/library/Fsub/part1a.ma +++ b/helm/software/matita/library/Fsub/part1a.ma @@ -176,7 +176,7 @@ cut (\forall G,T,Q.(JSubtype G T Q) \to |simplify;apply incl_nat_cons;assumption]]] |elim G2 0 [simplify;unfold;intros;assumption - |intro;elim s 0;simplify;intros;apply incl_nat_cons;assumption]]] + |intro;elim t 0;simplify;intros;apply incl_nat_cons;assumption]]] |intros 4;(*generalize in match H1;*)elim H1 [inversion H5 [intros;rewrite < H8;apply (SA_Top ? ? H2 H3) diff --git a/helm/software/matita/library/Fsub/util.ma b/helm/software/matita/library/Fsub/util.ma index 8b111e3f2..582114c69 100644 --- a/helm/software/matita/library/Fsub/util.ma +++ b/helm/software/matita/library/Fsub/util.ma @@ -35,7 +35,7 @@ let rec max m n \def [true \Rightarrow n |false \Rightarrow m]. -inductive in_list (A : Set) : A \to (list A) \to Prop \def +inductive in_list (A : Type) : A \to (list A) \to Prop \def | in_Base : \forall x:A.\forall l:(list A). (in_list A x (x :: l)) | in_Skip : \forall x,y:A.\forall l:(list A). diff --git a/helm/software/matita/library/list/sort.ma b/helm/software/matita/library/list/sort.ma index 939cecede..d182ed6d6 100644 --- a/helm/software/matita/library/list/sort.ma +++ b/helm/software/matita/library/list/sort.ma @@ -18,7 +18,7 @@ include "datatypes/bool.ma". include "datatypes/constructors.ma". include "list/list.ma". -let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝ +let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ match l with [ nil ⇒ false | (cons a l') ⇒ @@ -28,7 +28,7 @@ let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝ ] ]. -let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝ +let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝ match l with [ nil ⇒ true | (cons x l') ⇒ @@ -39,7 +39,7 @@ let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝ ] ]. -let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝ +let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝ match l with [ nil ⇒ [x] | (cons he l') ⇒ @@ -50,7 +50,7 @@ let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝ ]. lemma insert_ind : - ∀A:Set. ∀le: A → A → bool. ∀x. + ∀A:Type. ∀le: A → A → bool. ∀x. ∀P:(list A → list A → Prop). ∀H:(∀l: list A. l=[] → P [] [x]). ∀H2: @@ -86,7 +86,7 @@ lemma insert_ind : qed. -let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝ +let rec insertionsort (A:Type) (le: A → A → bool) (l: list A) on l ≝ match l with [ nil ⇒ [] | (cons he l') ⇒ @@ -95,7 +95,7 @@ let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝ ]. lemma ordered_injective: - ∀A:Set. ∀le:A → A → bool. + ∀A:Type. ∀le:A → A → bool. ∀l:list A. ordered A le l = true → ordered A le (tail A l) = true. intros 3 (A le l). elim l @@ -105,12 +105,12 @@ lemma ordered_injective: clear H1; elim l1; [ simplify; reflexivity; - | cut ((le s s1 \land ordered A le (s1::l2)) = true); + | cut ((le t t1 \land ordered A le (t1::l2)) = true); [ generalize in match Hcut; apply andb_elim; - elim (le s s1); + elim (le t t1); [ simplify; - fold simplify (ordered ? le (s1::l2)); + fold simplify (ordered ? le (t1::l2)); intros; assumption; | simplify; intros (Habsurd); @@ -126,7 +126,7 @@ lemma ordered_injective: qed. lemma insert_sorted: - \forall A:Set. \forall le:A\to A\to bool. + \forall A:Type. \forall le:A\to A\to bool. (\forall a,b:A. le a b = false \to le b a = true) \to \forall l:list A. \forall x:A. ordered A le l = true \to ordered A le (insert A le x l) = true. @@ -139,7 +139,7 @@ lemma insert_sorted: elim l'; simplify; [ rewrite > H5; reflexivity - | elim (le x s); simplify; + | elim (le x t); simplify; [ rewrite > H5; reflexivity | simplify in H4; @@ -157,7 +157,7 @@ lemma insert_sorted: qed. theorem insertionsort_sorted: - ∀A:Set. + ∀A:Type. ∀le:A → A → bool.∀eq:A → A → bool. (∀a,b:A. le a b = false → le b a = true) \to ∀l:list A. @@ -166,7 +166,7 @@ theorem insertionsort_sorted: elim l; [ simplify; reflexivity; - | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s); + | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) t); assumption; ] qed. \ No newline at end of file diff --git a/helm/software/matita/tests/discriminate.ma b/helm/software/matita/tests/discriminate.ma index 81c2da87f..b1d7b9ca6 100644 --- a/helm/software/matita/tests/discriminate.ma +++ b/helm/software/matita/tests/discriminate.ma @@ -13,24 +13,15 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/discriminate". -include "../legacy/coq.ma". -alias id "not" = "cic:/Coq/Init/Logic/not.con". -alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". -alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". -alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". -alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)". -alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". -alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". - -inductive foo: Prop \def I_foo: foo. - -alias num (instance 0) = "binary integer number". + +include "logic/equality.ma". +include "nat/nat.ma". +include "datatypes/constructors.ma". + theorem stupid: - 1 = 0 \to (\forall p:Prop. p \to not p). + (S O) = O \to (\forall p:Prop. p \to Not p). intros. - generalize in match I_foo. + generalize in match I. destruct H. qed. @@ -38,7 +29,6 @@ inductive bar_list (A:Set): Set \def | bar_nil: bar_list A | bar_cons: A \to bar_list A \to bar_list A. - theorem stupid2: \forall A:Set.\forall x:A.\forall l:bar_list A. bar_nil A = bar_cons A x l \to False. @@ -69,3 +59,64 @@ theorem recursive: S (S (S O)) = S (S O) \to False. intros; destruct H. qed. + +inductive complex (A,B : Type) : B → A → Type ≝ +| C1 : ∀x:nat.∀a:A.∀b:B. complex A B b a +| C2 : ∀a,a1:A.∀b,b1:B.∀x:nat. complex A B b1 a1 → complex A B b a. + + +theorem recursive1: ∀ x,y : nat. + (C1 ? ? O (Some ? x) y) = + (C1 ? ? (S O) (Some ? x) y) → False. +intros; destruct H; +qed. + +theorem recursive2: ∀ x,y,z,t : nat. + (C1 ? ? t (Some ? x) y) = + (C1 ? ? z (Some ? x) y) → t=z. +intros; destruct H;assumption. +qed. + +theorem recursive3: ∀ x,y,z,t : nat. + C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) = + C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t. +intros; destruct H;assumption. +qed. + +theorem recursive4: ∀ x,y,z,t : nat. + C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? z) y) = + C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t. +intros; + + + + + (λHH : ((C1 (option nat) nat (S O) (Some nat -7) -8) = (C1 (option nat) nat (S O) (Some nat -9) -8)) + eq_elim_r + (complex (option nat) nat -8 (Some nat -7)) + (C1 (option nat) nat (S O) (Some nat -9) -8) + (λc:(complex (option nat) nat -8 (Some nat -7)). + (eq (option nat) + ((λx:(complex (option nat) nat -8 (Some nat -7)). + match x return (λy1:nat.(λy2:(option nat).(λ x:(complex (option nat) nat y1 y2).(option nat)))) with + [ (C1 (y1:nat) (a:(option nat)) (b:nat)) => a + | (C2 (a:(option nat)) (a1:(option nat)) (b:nat) (b1:nat) (y2:nat) (y3:(complex (option nat) nat b1 a1))) ⇒ + (Some nat -7) + ]) c) + (Some nat -9))) + ? + (C1 (option nat) nat (S O) (Some nat -7) -8) + HH) + + + + +destruct H;assumption. +qed. + +theorem recursive2: ∀ x,y : nat. + C2 ? ? (None ?) ? (S O) ? O (C1 ? ? O (Some ? x) y) = + C2 ? ? (None ?) ? (S O) ? O (C1 ? ? (S O) (Some ? x) y) → False. +intros; destruct H; + + -- 2.39.2