michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

doc(examples/standard/constable): add section delimiters

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-28 01:17:31 -07:00
parent fb56767e07
commit acf8a4261b
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
examples/standard/constable.lean
View file

@ -1,8 +1,9 @@
-- Theorems/Exercises from "Logical Investigations, with the Nuprl Proof Assistant" -- Theorems/Exercises from "Logical Investigations, with the Nuprl Proof Assistant"
-- by Robert L. Constable and Anne Trostle -- by Robert L. Constable and Anne Trostle
-- http://www.nuprl.org/MathLibrary/LogicalInvestigations/ -- http://www.nuprl.org/MathLibrary/LogicalInvestigations/
import standard import logic
-- 2. The Minimal Implicational Calculus
theorem thm1 {A B : Prop} : A → B → A theorem thm1 {A B : Prop} : A → B → A
:= assume Ha Hb, Ha := assume Ha Hb, Ha
@ -14,6 +15,7 @@ theorem thm3 {A B C : Prop} : (A → B) → (B → C) → (A → C)
:= assume Hab Hbc Ha, := assume Hab Hbc Ha,
Hbc (Hab Ha) Hbc (Hab Ha)
-- 3. False Propositions and Negation
theorem thm4 {P Q : Prop} : ¬P → P → Q theorem thm4 {P Q : Prop} : ¬P → P → Q
:= assume Hnp Hp, := assume Hnp Hp,
absurd_elim Q Hp Hnp absurd_elim Q Hp Hnp
@ -37,6 +39,7 @@ theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q)
have H : P → Q, from assume H', Hq, have H : P → Q, from assume H', Hq,
absurd H Hn absurd H Hn
-- 4. Conjunction and Disjunction
theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P) theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P)
:= assume (em : P ∨ ¬P) (Hnn : ¬¬P), := assume (em : P ∨ ¬P) (Hnn : ¬¬P),
or_elim em or_elim em
@ -93,9 +96,9 @@ theorem thm16 {P Q : Prop} : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)) → ¬P
(assume Hq : Q, or_inr Hq) (assume Hq : Q, or_inr Hq)
(assume Hnq : ¬Q, or_inl (mt Hpq Hnq))) (assume Hnq : ¬Q, or_inl (mt Hpq Hnq)))
-- 5. First-Order Logic: All and Exists
section section
parameters {T : Type} {C : Prop} {P : T → Prop} parameters {T : Type} {C : Prop} {P : T → Prop}
theorem thm17a : (C → ∀x, P x) → (∀x, C → P x) theorem thm17a : (C → ∀x, P x) → (∀x, C → P x)
:= assume H : C → ∀x, P x, := assume H : C → ∀x, P x,
take x : T, assume Hc : C, take x : T, assume Hc : C,
@ -209,4 +212,4 @@ theorem thm24b : (∃x : T, true) → (∀x, P x ∧ C) → (∀x, P x) ∧ C
have Hx : ∀x, P x, from take x, and_elim_left (H x), have Hx : ∀x, P x, from take x, and_elim_left (H x),
and_intro Hx Hc and_intro Hx Hc
end -- of section end -- of section