Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
(assume h : p ∧ (q ∨ r),
have hp : p, from h.left,
or.elim h.right
(assume hq, or.inl ⟨hp, hq⟩)
(assume hr, or.inr ⟨hp, hr⟩))
(assume h : (p ∧ q) ∨ (p ∧ r),
or.elim h
(assume hpq,
have hp : p, from hpq.left,
have hq : q, from hpq.right,
⟨hp, or.inl hq⟩)
(assume hpr,
have hp : p, from hpr.left,
have hr : r, from hpr.right,
⟨hp, or.inr hr⟩))
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
(λ h : p ∧ (q ∨ r),
(λ hp : p,
or.elim h.right
(λ hq, or.inl $ and.intro hp hq)
(λ hr, or.inr $ and.intro hp hr))
h.left)
(λ h : (p ∧ q) ∨ (p ∧ r),
or.elim h
(λ hpq : p ∧ q,
(λ hp : p,
(λ hq: q,
and.intro hp (or.inl hq))
hpq.right)
hpq.left)
(λ hpr : p ∧ r,
(λ hp : p,
(λ hr : r,
and.intro hp (or.inr hr))
hpr.right)
hpr.left))
/-
propositions_as_types.lean:455:4: error
type mismatch at application
or.elim h (λ (hpq : p ∧ q),
(λ (hp : p),
(λ (hq : q),
⟨hp, or.inl hq⟩)
(hpq.right))
(hpq.left))
term
λ (hpq : p ∧ q),
(λ (hp : p),
(λ (hq : q),
⟨hp, or.inl hq⟩)
(hpq.right))
(hpq.left)
has type
∀ (hpq : p ∧ q), p ∧ (q ∨ ?m_1[hpq, _, _])
but is expected to have type
p ∧ q → p ∧ (q ∨ r)
propositions_as_types.lean:455:4: error
type mismatch at application
or.elim h ⁇
(λ (hpr : p ∧ r),
(λ (hp : p),
(λ (hr : r),
⟨hp, or.inr hr⟩)
(hpr.right))
(hpr.left))
term
λ (hpr : p ∧ r), (λ (hp : p), (λ (hr : r), ⟨hp, or.inr hr⟩) (hpr.right)) (hpr.left)
has type
∀ (hpr : p ∧ r), p ∧ (?m_1[hpr, _, _] ∨ r)
but is expected to have type
p ∧ r → p ∧ (q ∨ r)
-/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.