X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fbounded_quantifiers.ma;fp=weblib%2Farithmetics%2Fbounded_quantifiers.ma;h=6eef112e37ceb6143b49ac1409ae74c76670beb9;hb=adfe42bbd5aaa4130a4133f345930e79444f0f3e;hp=0000000000000000000000000000000000000000;hpb=4672640dc168a3adcbea86887c38d895358288e8;p=helm.git

diff --git a/weblib/arithmetics/bounded_quantifiers.ma b/weblib/arithmetics/bounded_quantifiers.ma
new file mode 100644
index 000000000..6eef112e3
--- /dev/null
+++ b/weblib/arithmetics/bounded_quantifiers.ma
@@ -0,0 +1,51 @@
+include "arithmetics/nat.ma".
+
+img class="anchor" src="icons/tick.png" id="decidable_not"lemma decidable_not: ∀P. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a P → a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (a title="logical not" href="cic:/fakeuri.def(1)"¬/aP).
+#P * #H [%2 % * /span class="autotactic"2span class="autotrace" trace /span/span/ | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/] 
+qed.
+
+img class="anchor" src="icons/tick.png" id="decidable_or"lemma decidable_or: ∀P,Q. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a P → a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a Q → a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (Pa title="logical or" href="cic:/fakeuri.def(1)"∨/aQ).
+#P #Q * #HP [#_ %1 %1 // |* #HQ [ %1 %2 // | %2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] 
+qed.
+
+img class="anchor" src="icons/tick.png" id="decidable_forall"lemma decidable_forall: ∀P. (∀i.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (P i))→ 
+  ∀n.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → P i).
+#P #Hdec #n elim n
+  [%1 #i #lti0 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … lti0) @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //
+  |#m * #H
+    [cases (Hdec m) #HPm
+      [%1 #i #lei0 cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lei0) #H1
+        [@H @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H1 |>(a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a … H1) @HPm]
+      |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … HPm) #H1 @H1 //
+      ]
+    |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 #i #leim @H1 @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //
+    ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="not_exists_to_forall"lemma not_exists_to_forall: ∀P,n.
+  a title="logical not" href="cic:/fakeuri.def(1)"¬/a(a title="exists" href="cic:/fakeuri.def(1)"∃/ai. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a P i) → ∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a title="logical not" href="cic:/fakeuri.def(1)"¬/a P i.
+#P #n elim n 
+  [#_ #i #lti0 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … lti0) @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //
+  |#m #Hind #H1 #i #leiS cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … leiS) #H2
+    [@(Hind … (a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a … H2)) @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) *
+     #a * #leam #Pa %{a} % // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //
+    |@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) #Pi %{i} % //
+    ]
+  ]
+qed. 
+ 
+img class="anchor" src="icons/tick.png" id="not_forall_to_exists"lemma not_forall_to_exists: ∀P,n. (∀i.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (P i)) → 
+  a title="logical not" href="cic:/fakeuri.def(1)"¬/a(∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → P i) → (a title="exists" href="cic:/fakeuri.def(1)"∃/ai. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a (P i)).
+#P #n #decP elim n
+  [* #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @H #i #lti0 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … lti0) @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //
+  |#m #Hind #H1 cases (decP m) #H2
+    [cases (Hind ?)
+      [#i * #leim #nPi %{i} % // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //
+      |@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) #H3 #i #leiS cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … leiS)
+        [#ltiS @H3 @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a // |#eqi //]
+      ]
+    |%{m} % //
+    ]
+  ]
+qed.
\ No newline at end of file