example.lean

-- import data.int.basic  -- no mathlib yet

#print "hello world"

#eval 2+3

lemma test (P Q R : Prop) : ((P ∨ Q → R) ∧ P) → R :=
begin
  intro hyp,
  cases hyp with h h',
  apply h,
  exact or.inl h'
end

#check test

variable (α : Type)

theorem ext {a b : set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (assume x, propext (h x))

example (X : Type) (A B C : set X) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) :=
begin
  apply ext,
  intro x,
  split ; intro h,
  { cases h with h' h'',
    cases h'',
    { apply or.inl,
      exact ⟨h', h''⟩},
      apply or.inr,
      exact ⟨h', h''⟩},
  { cases h with h' h'',
    { cases h' with h₁ h₂,
      exact ⟨h₁, or.inl h₂⟩ },
    { cases h'' with h₁ h₂,
      exact ⟨h₁, or.inr h₂⟩ }}
end

--[@derive decidable_eq] -- must be mathlib I guess
inductive three : Type
| zero : three
| one : three
| two : three

open three

#print decidable
#print three.no_confusion

-- why can I not write "three.no_confusion"?
instance : decidable_eq three :=
begin
  intros a b,
  cases a;cases b,
  exact decidable.is_true rfl,
  exact decidable.is_false (λ x, three.no_confusion x),
  exact decidable.is_false (λ x, three.no_confusion x),
  exact decidable.is_false (λ x, three.no_confusion x),
  exact decidable.is_true rfl,
  exact decidable.is_false (λ x, three.no_confusion x),
  exact decidable.is_false (λ x, three.no_confusion x),
  exact decidable.is_false (λ x, three.no_confusion x),
  exact decidable.is_true rfl,
end

#check nat.mul_le_mul_left

example (n :  ℕ) : n * n ≠ 2 :=
begin
  cases n,exact dec_trivial,
  cases n,exact dec_trivial,
  apply ne_of_gt,
  suffices : 2 < 2 * (n + 2),
    refine lt_of_lt_of_le this _,
    apply nat.mul_le_mul_right,exact dec_trivial,
  refine lt_of_lt_of_le (show 2 < 2 * 2, from dec_trivial) _,
  apply nat.mul_le_mul_left,
  exact dec_trivial,
--  trace_state -- because I can't see the goal
end