From 11852aa9c64848457d84af63186d2317772e74bf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 20:06:29 +0000 Subject: [PATCH] Dummy dependent types are no longer cleaned in inductive type arities. --- .../matita/contribs/POPLmark/Fsub/defn.ma | 22 +++++++++---------- .../matita/contribs/POPLmark/Fsub/part1a.ma | 1 - .../POPLmark/Fsub/part1a_inversion.ma | 1 - .../matita/contribs/POPLmark/Fsub/util.ma | 3 +-- 4 files changed, 12 insertions(+), 15 deletions(-) diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma index 95c832efd..184166ed9 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Fsub/defn". include "Fsub/util.ma". (*** representation of Fsub types ***) @@ -153,18 +152,19 @@ intros 2;elim G [elim H;elim H1;lapply (not_in_list_nil ? ? H2);elim Hletin |elim H1;elim H2;elim (in_list_cons_case ? ? ? ? H3) [rewrite < H4;simplify;apply in_list_head - |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a); - apply (ex_intro ? ? a1);assumption]] + |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a1); + apply (ex_intro ? ? a2);assumption]] qed. 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 (not_in_list_nil ? ? H);elim Hletin - |intros 3;elim t;simplify in H1;elim (in_list_cons_case ? ? ? ? H1) - [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_list_head - |elim (H H2);elim H3;apply (ex_intro ? ? a); - apply (ex_intro ? ? a1);apply in_list_cons;assumption]] + |intros 3; + elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1) + [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t);apply in_list_head + |elim (H H2);elim H3;apply (ex_intro ? ? a1); + apply (ex_intro ? ? a2);apply in_list_cons;assumption]] qed. lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to @@ -200,7 +200,7 @@ lemma fv_env_extends : \forall H,x,B,C,T,U,G. (fv_env (H @ ((mk_bound B x T) :: G))) = (fv_env (H @ ((mk_bound C x U) :: G))). intros;elim H - [simplify;reflexivity|elim t;simplify;rewrite > H1;reflexivity] + [simplify;reflexivity|elim a;simplify;rewrite > H1;reflexivity] qed. lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. @@ -237,12 +237,12 @@ cut (\forall l:(list nat).\exists n.\forall m. |intros;elim l [apply (ex_intro ? ? O);intros;unfold;intro;elim (not_in_list_nil ? ? H1) |elim H; - apply (ex_intro ? ? (S (max a t))). + apply (ex_intro ? ? (S (max a1 a))). intros.unfold. intro. elim (in_list_cons_case ? ? ? ? H3) [rewrite > H4 in H2.autobatch |elim H4 - [apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch + [apply (H1 m ? H4).apply (trans_le ? (max a1 a));autobatch |assumption]]]] qed. @@ -309,7 +309,7 @@ intros 7;elim H 0 [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4) |destruct H8;apply (WFE_cons ? ? ? ? H4 H6 H2)] - |intros;simplify;generalize in match H2;elim t;simplify in H4; + |intros;simplify;generalize in match H2;elim a;simplify in H4; inversion H4;intros [destruct H5 |destruct H9;apply WFE_cons diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma index fc3621618..7ae8763cf 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Fsub/part1a/". include "Fsub/defn.ma". (*** Lemma A.1 (Reflexivity) ***) diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma index b538f4d3a..5a472e640 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Fsub/part1a_inversion/". include "Fsub/defn.ma". (*** Lemma A.1 (Reflexivity) ***) diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma index bd7018d3c..3521e87dd 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Fsub/util". include "logic/equality.ma". include "nat/compare.ma". include "list/list.ma". @@ -55,4 +54,4 @@ lemma max_case : \forall m,n.(max m n) = match (leb m n) with [ true \Rightarrow n | false \Rightarrow m ]. intros;elim m;simplify;reflexivity; -qed. \ No newline at end of file +qed. -- 2.39.2