-- This file:
--   http://anggtwu.net/LEAN/propsandproofs1.lean.html
--   http://anggtwu.net/LEAN/propsandproofs1.lean
--          (find-angg "LEAN/propsandproofs1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/propsandproofs1.lean"))

-- (find-tpinleanpage (+ 6 23) "3 Propositions and Proofs")
-- (find-tpinleanpage (+ 6 23) "3.1 Propositions as Types")
-- (find-tpinleantext (+ 6 23) "3.1 Propositions as Types")
-- (find-tpinleanpage (+ 6 25) "3.2 Working with Propositions as Types")
-- (find-tpinleanpage (+ 6 25)   "theorem t1 : p → q → p := λ hp : p, λ hq : q, hp")
-- (find-tpinleantext (+ 6 25)   "theorem t1 : p → q → p := λ hp : p, λ hq : q, hp")
-- (find-tpinleanpage (+ 6 25)   "show p, from hp")
-- (find-tpinleantext (+ 6 25)   "show p, from hp")
-- (find-tpinleanpage (+ 6 27) "3.3 Propositional Logic")
-- (find-tpinleanpage (+ 6 28)     "The example command")
-- (find-tpinleantext (+ 6 28)     "The example command")
-- (find-tpinleanpage (+ 6 31) "3.4 Introducing Auxiliary Subgoals")
-- (find-tpinleanpage (+ 6 32) "3.5 Classical Logic")
-- (find-tpinleanpage (+ 6 33) "3.6 Examples of Propositional Validities")
-- (find-tpinleanpage (+ 6 35) "3.7 Exercises")
-- (find-lean4file "src/Init/Classical.lean")

-- (find-tpinlean4page  22 "3. Propositions and Proofs")
-- (find-tpinlean4text  22    "Propositions and Proofs")
-- (find-tpinlean4page  22 "3.1. Propositions as Types")
-- (find-tpinlean4text  22      "Propositions as Types")
-- (find-tpinlean4page  25 "3.2. Working with Propositions as Types")
-- (find-tpinlean4text  25      "Working with Propositions as Types")
-- (find-tpinlean4page  28 "3.3. Propositional Logic")
-- (find-tpinlean4text  28      "Propositional Logic")
-- (find-tpinlean4page  33 "3.4. Introducing Auxiliary Subgoals")
-- (find-tpinlean4text  33      "Introducing Auxiliary Subgoals")
-- (find-tpinlean4page  34 "3.5. Classical Logic")
-- (find-tpinlean4text  34      "Classical Logic")
-- (find-tpinlean4page  35 "3.6. Examples of Propositional Validities")
-- (find-tpinlean4text  35      "Examples of Propositional Validities")
-- (find-tpinlean4file "propositions_and_proofs.md")
-- (find-tpinlean4file "propositions_and_proofs.md" "Propositions as Types")
-- (find-tpinlean4file "propositions_and_proofs.md" "``(fun x => t) s`` and ``t[s/x]``")
-- (find-tpinlean4file "propositions_and_proofs.md" "``theorem`` command is really a version of")
-- (find-tpinlean4file "propositions_and_proofs.md" "to the left of the colon")

-- open Classical

def Implies (p q : Prop) : Prop := p → q
#check And     -- Prop → Prop → Prop
#check And     -- Prop → Prop → Prop
#check Or      -- Prop → Prop → Prop
#check Not     -- Prop → Prop
#check Implies -- Prop → Prop → Prop

variable (p q r : Prop)
#check And p q                      -- Prop
#check Or (And p q) r               -- Prop
#check Implies (And p q) (And q p)  -- Prop

-- def Implies (p q : Prop) : Prop := p → q
structure Proof (p : Prop) : Type where
  proof : p
#check Proof   -- Proof : Prop → Type
#print Proof   -- Proof : Prop → Type

axiom and_comm (p q : Prop) : Proof (Implies (And p q) (And q p))
axiom modus_ponens  : (p q : Prop) → Proof (Implies p q) → Proof p → Proof q
axiom implies_intro : (p q : Prop) → (Proof p → Proof q) → Proof (Implies p q)


variable (p q : Prop)
#check and_comm
#check and_comm p q     -- Proof (Implies (And p q) (And q p))

variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

-- theorem t1 : p → q → p := fun hp : p => fun hq : q => show p from hp

-- theorem t1              (hp : p) (hq : q) : p := hp
-- theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp

axiom hp : p

theorem t2 : q → p := t1 hp

#print t1

-- (find-tpinlean4file "propositions_and_proofs.md" "axiom unsound : False")
-- (find-tpinlean4file "propositions_and_proofs.md" "show p from hp")

-- theorem t1 : ∀ {p q : Prop}, p → q → p := fun {p q : Prop} (hp : p) (hq : q) => hp
-- theorem t1 : p → q → p := fun (hp : p) (hq : q) => hp
-- theorem t1 : q → p := fun (hq : q) => hp

-- theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp

variable (p q r s : Prop)

#check t1 p q                -- p → q → p
#check t1 r s                -- r → s → r
#check t1 (r → s) (s → r)    -- (r → s) → (s → r) → r → s

variable (h : r → s)
#check t1 (r → s) (s → r) h  -- (s → r) → r → s



-- theorem t2 {P Q : prop} («P» : P) («P→Q» : P → Q) : Q := «P→Q» «P»




-- variable p : Prop
#check em p

constant and     : Prop → Prop → Prop
constant or      : Prop → Prop → Prop
constant not     : Prop → Prop
constant implies : Prop → Prop → Prop

variables p q r : Prop
#check and p q                                    -- Prop
#check or (and p q) r                             -- Prop
#check implies (and p q) (and q p)                -- Prop

constant Proof : Prop → Type

constant and_comm : Π p q : Prop,
  Proof (implies (and p q) (and q p))

variables p q : Prop
#check and_comm p q                -- Proof (implies (and p q) (and q p))

constant modus_ponens :
  Π p q : Prop, Proof (implies p q) →                       Proof p → Proof q

constant implies_intro :
  Π p q : Prop, (Proof p → Proof q) → Proof (implies p q).





-- Local Variables:
-- coding:  utf-8-unix
-- End: