From 7f6235dca57343e63217316b6415599daef7d4aa Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 6 Jul 2012 12:12:46 +0000 Subject: [PATCH] manual --- weblib/arithmetics/nat.ma | 3 ++- weblib/basics/bool.ma | 11 ----------- weblib/basics/logic.ma | 2 +- 3 files changed, 3 insertions(+), 13 deletions(-) diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma index a592b1377..b735e1210 100644 --- a/weblib/arithmetics/nat.ma +++ b/weblib/arithmetics/nat.ma @@ -1116,4 +1116,5 @@ lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i. #i #n #m #leni #lemi normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) -normalize // qed. \ No newline at end of file +normalize // qed. + diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma index a32d67a0a..bd832f5f9 100644 --- a/weblib/basics/bool.ma +++ b/weblib/basics/bool.ma @@ -100,14 +100,3 @@ notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp definition ite ≝ λA:Type[0].λe.λt,f:A.match e with [ true ⇒ t | false ⇒ f ]. interpretation "if then else" 'ite e t f = (ite ? e t f). - -(* axiom foo : ∀b.a title="if then else" href="cic:/fakeuri.def(1)"£/a b & a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a & a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. *) -axiom foo : ∀b. if b then True else False. - -(*theorem bool_to_decidable_eq: - ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (b1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ab2). -#b1 #b2 (cases b1) (cases b2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ %2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ qed. - -theorem true_or_false: -∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. -#b (cases b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.*) \ No newline at end of file diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma index b9dfed28c..527e48429 100644 --- a/weblib/basics/logic.ma +++ b/weblib/basics/logic.ma @@ -269,4 +269,4 @@ qed. theorem streicherK : ∀T:Type[2].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[3].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p. #T #t #P #H #p >(a href="cic:/matita/basics/logic/lemmaK.def(2)"lemmaK/a T t p) @H -qed. \ No newline at end of file +qed. -- 2.39.2