/- To compile:
     alectryon corner_cases.lean3 -o corner_cases.lean3.html
       # Lean → HTML; produces ‘corner_cases.lean3.html’ -/

example : true := begin
true
  trivial

--- asda
end

example : true := begin
true
    skip,
true exact by trivial, done
end

example : true :=
begin
true
  exact by {
    skip,
    by_contra,
    apply h,
    exact trivial
  },
  skip
end

#check 1
1 : ℕ
#check (1 +
        1 +
        1)
1 + 1 + 1 : ℕ

theorem t0 : true -> true :=
  by
true → true {
true → true intro,
ᾰ: true
true exact true.intro }

theorem t1 : true -> true :=
  begin
true → true
    -- ⊢ true → true
    intro,
ᾰ: true
true
    -- ᾰ : true ⊢ true
    exact true.intro
  end

-- theorem x : "a" = 1.

theorem t2 : true -> true -> true :=
  begin
true → true → true
    repeat { intro } ,
ᾰ, ᾰ_1: true
true
    sorry
  end

theorem t3 : true -> true -> true :=
  begin
true → true → true
    exact by { repeat { intro }, assumption }
  end

theorem t4 : true -> true -> true :=
  by
true → true → true {
true → true → true repeat { intro },
ᾰ, ᾰ_1: true
true admit }

example : true := by
true exact true.intro
example : true := by
true trivial

example (a b c : ℕ) (H1 : a = b + 1) (H2 : b = c) : a = c + 1 :=
calc a = b + 1 : by
a, b, c: ℕ
H1: a = b + 1
H2: b = c
a = b + 1 exact H1
...    = c + 1 : by
a, b, c: ℕ
H1: a = b + 1
H2: b = c
b + 1 = c + 1 rw [ by exact H2 ]

example (a b c : ℕ) : a * (b * c) = a * (c * b) :=
begin
a, b, c: ℕ
a * (b * c) = a * (c * b)
  conv
  begin          -- | a * (b * c) = a * (c * b)
    to_lhs,      -- | a * (b * c)
    congr,       -- 2 goals : | a and | b * c
    skip,        -- | b * c
    rw nat.mul_comm -- | c * b
  end
end

example : true := begin
true
    skip <|> skip,
true /- Second skip not executed -/
    done <|> skip,
true
    trivial
end

example (n : ℕ) : n = n := by
n: ℕ
n = n {
n: ℕ
n = n
    induction n,
nat.zero
0 = 0
n_n: ℕ
n_ih: n_n = n_n
nat.succ
n_n.succ = n_n.succ
    simp,
n_n: ℕ
n_ih: n_n = n_n
nat.succ
n_n.succ = n_n.succ
    simp
}

example (n : ℕ) : n = n :=
begin
n: ℕ
n = n
  induction n,
nat.zero
0 = 0
n_n: ℕ
n_ih: n_n = n_n
nat.succ
n_n.succ = n_n.succ
  simp,
n_n: ℕ
n_ih: n_n = n_n
nat.succ
n_n.succ = n_n.succ
  simp
end

example (n : ℕ) : n = n := by
n: ℕ
n = n induction n ; simp

-- grouped as (((skip ; skip) ; induction n) ; skip) ; simp
example (n : ℕ) : n = n :=
  by
n: ℕ
n = n skip ; skip ; induction n ; skip ; simp

example (n : ℕ) : n = n := begin
n: ℕ
n = n
    induction n,
nat.zero
0 = 0
n_n: ℕ
n_ih: n_n = n_n
nat.succ
n_n.succ = n_n.succ {
nat.zero
0 = 0 simp },
    simp
end

example : ∀ (n a : ℕ), n = n := begin
∀ (n : ℕ), ℕ → n = n
    repeat { intro },
n, a: ℕ
n = n simp
end

example : true := begin
true
    try { done },
true try { trivial }
end

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) :=
begin
p, q, r: Prop
p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r
  intro h,
p, q, r: Prop
h: p ∧ (q ∨ r)
p ∧ q ∨ p ∧ r
  cases h with hp hqr,
p, q, r: Prop
hp: p
hqr: q ∨ r
p ∧ q ∨ p ∧ r
  show (p ∧ q) ∨ (p ∧ r),
p, q, r: Prop
hp: p
hqr: q ∨ r
p ∧ q ∨ p ∧ r
  cases hqr with hq hr,
p, q, r: Prop
hp: p
hq: q
or.inl
p ∧ q ∨ p ∧ r
p, q, r: Prop
hp: p
hr: r
or.inr
p ∧ q ∨ p ∧ r
  {
p, q, r: Prop
hp: p
hq: q
or.inl
p ∧ q ∨ p ∧ r have hpq : p ∧ q,
p, q, r: Prop
hp: p
hq: q
p ∧ q
      split ; assumption ,
p, q, r: Prop
hp: p
hq: q
hpq: p ∧ q
p ∧ q ∨ p ∧ r
    left,
p, q, r: Prop
hp: p
hq: q
hpq: p ∧ q
p ∧ q exact hpq },
  have hpr : p ∧ r,
p, q, r: Prop
hp: p
hr: r
p ∧ r
    split ; assumption,
p, q, r: Prop
hp: p
hr: r
hpr: p ∧ r
p ∧ q ∨ p ∧ r
  right,
p, q, r: Prop
hp: p
hr: r
hpr: p ∧ r
p ∧ r
  exact hpr
end

example (p q r : Prop) (hp : p) (hq : q) (hr : r) :
  p ∧ q ∧ r :=
begin
p, q, r: Prop
hp: p
hq: q
hr: r
p ∧ q ∧ r
  split,
p, q, r: Prop
hp: p
hq: q
hr: r
p
p, q, r: Prop
hp: p
hq: q
hr: r
q ∧ r
  all_goals { try { split } },
p, q, r: Prop
hp: p
hq: q
hr: r
p
p, q, r: Prop
hp: p
hq: q
hr: r
q
p, q, r: Prop
hp: p
hq: q
hr: r
r
  all_goals { assumption }
end

example (p q r : Prop) (hp : p) (hq : q) (hr : r) :
  p ∧ q ∧ r :=
begin
p, q, r: Prop
hp: p
hq: q
hr: r
p ∧ q ∧ r
  repeat { all_goals { split <|> assumption } }
end

example :true := begin
true
  skip,
true skip; trivial
end

example (n m k : ℕ) (h1 : n = m) (h2 : m = k): (n = k) :=
begin
n, m, k: ℕ
h1: n = m
h2: m = k
n = k
    rw [show n = m, by assumption, show m = k, by assumption]
end

theorem sub_le_sub_left {n m : ℕ} (k) (h : n ≤ m) : k - m ≤ k - n :=
begin
n, m, k: ℕ
h: n ≤ m
k - m ≤ k - n
  induction h; [refl, exact le_trans (nat.pred_le _) h_ih]
end


example : true := by
true {
true
  try { trivial }
}

example : true := by
true begin
true
  try begin trivial end
end

-- grouped as done <|> (done <|> trivial)
example : true := by
true done <|> done <|> trivial

-- unexecuted tactic at end
example : true := by
true {
true trivial ; done }

-- special notation
example (n : nat) : true :=
   by
n: ℕ
true induction n ; [skip, skip]; [trivial, trivial]

example : true := begin
true
skip,
true
trivial, -- trailing comma
end

-- trailing comma
example : true := by
true {
true skip ; trivial, }

example : true := by
true {
true { skip ; [skip, skip] } <|> trivial}

example : true := by
true {
true {{{{ skip ; [skip, skip] }}}} <|> trivial}


-- { } block with no executed children
-- there is no first goal to focus on
example : true := begin
true { trivial , { skip, skip } } <|> trivial end


-- trailing comma
example : true := begin
true {
true skip ; trivial, } end

example : true := begin
true {
true { skip ; [skip, skip] } <|> trivial} end

example : true := begin
true {
true {{{{ skip ; [skip, skip] }}}} <|> trivial} end