From: Andrea Asperti Date: Mon, 21 Mar 2011 08:18:22 +0000 (+0000) Subject: sn_prod X-Git-Tag: make_still_working~2557 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=078fb4b522a283459a70c2a8c9398e84fc1deeb5;p=helm.git sn_prod --- diff --git a/matita/matita/lib/lambda/reduction.ma b/matita/matita/lib/lambda/reduction.ma index 8d0cefc16..44a8e6f26 100644 --- a/matita/matita/lib/lambda/reduction.ma +++ b/matita/matita/lib/lambda/reduction.ma @@ -65,6 +65,21 @@ lemma red_lambda : ∀M,N,P. red (Lambda M N) P → ] qed. +lemma red_prod : ∀M,N,P. red (Prod M N) P → + (∃M1. P = (Prod M1 N) ∧ red M M1) ∨ + (∃N1. P = (Prod M N1) ∧ red N N1). +#M #N #P #redMNP (inversion redMNP) + [#P1 #M1 #N1 #eqH destruct + |2,3: #M1 #N1 #eqH destruct + |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct + |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 + (@(ex_intro … M1)) % // + |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2 + (@(ex_intro … N1)) % // + |#Q1 #M1 #red1 #_ #eqH destruct + ] +qed. + definition reduct ≝ λn,m. red m n. definition SN ≝ WF ? reduct. @@ -159,7 +174,7 @@ qed. lemma SH_to_SN: ∀N. SH N → SN N. @WF_antimonotonic /2/ qed. -lemma SH_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M). +lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M). #N #snN (elim snN) #P #shP #HindP #M #snM (* for M we proceed by induction on SH *) (lapply (SN_to_SH ? snM)) #shM (elim shM) @@ -186,7 +201,14 @@ lemma SH_Lambda: ∀N.SH N → ∀M.SH M → SN (Lambda N M). ] qed. *) - +lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M). +#N #snN (elim snN) #P #shP #HindP #M #snM (elim snM) +#Q #snQ #HindQ % #a #redH (cases (red_prod … redH)) + [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) // + % /2/ + |* #S * #eqa #redQS >eqa @(HindQ S) /2/ + ] +qed.