76 lines
2.6 KiB
Text
76 lines
2.6 KiB
Text
inductive L (α : Type u) : Type u where
|
||
| nil : L α
|
||
| cons (x : α) (xs : L α) : L α
|
||
|
||
-- Check that L.cons.inj uses the per-ctor noConfusion principle
|
||
/--
|
||
info: theorem L.cons.inj.{u} : ∀ {α : Type u} {x : α} {xs : L α} {x_1 : α} {xs_1 : L α},
|
||
L.cons x xs = L.cons x_1 xs_1 → x = x_1 ∧ xs = xs_1 :=
|
||
fun {α} {x} {xs} {x_1} {xs_1} x_2 => L.cons.noConfusion x_2 fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
|
||
-/
|
||
#guard_msgs in
|
||
#print L.cons.inj
|
||
|
||
-- Check that injection uses the per-ctor noConfusion principle
|
||
|
||
theorem ex1 (h : L.cons x xs = L.cons y ys) : x = y ∧ xs = ys := by
|
||
injection h
|
||
repeat constructor <;> assumption
|
||
|
||
/--
|
||
info: theorem ex1.{u_1} : ∀ {α : Type u_1} {x : α} {xs : L α} {y : α} {ys : L α},
|
||
L.cons x xs = L.cons y ys → x = y ∧ xs = ys :=
|
||
fun {α} {x} {xs} {y} {ys} h => L.cons.noConfusion h fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
|
||
-/
|
||
#guard_msgs in #print ex1
|
||
|
||
-- Check that injection does not intro more than it should
|
||
theorem ex2 (h : L.cons x xs = L.cons y ys) : Unit → x = y ∧ xs = ys := by
|
||
injection h
|
||
intro u
|
||
repeat constructor <;> assumption
|
||
|
||
-- Check that grind uses `L.cons.noConfusion`
|
||
|
||
theorem ex3 (h : L.cons x xs = L.cons y ys) : x = y ∧ xs = ys := by
|
||
grind
|
||
/--
|
||
info: theorem ex3._proof_1_1.{u_1} : ∀ {α : Type u_1} {x : α} {xs : L α} {y : α} {ys : L α},
|
||
L.cons x xs = L.cons y ys → x = y ∧ xs = ys :=
|
||
fun {α} {x} {xs} {y} {ys} h =>
|
||
Classical.byContradiction
|
||
(Lean.Grind.intro_with_eq (¬(x = y ∧ xs = ys)) (¬x = y ∨ ¬xs = ys) False (Lean.Grind.not_and (x = y) (xs = ys))
|
||
fun h_1 =>
|
||
id
|
||
(Eq.mp
|
||
(Eq.trans (Eq.symm (eq_true (id (L.cons.inj (id h)).1)))
|
||
(Lean.Grind.eq_false_of_not_eq_true
|
||
(Eq.trans
|
||
(Eq.symm
|
||
(Lean.Grind.or_eq_of_eq_false_right
|
||
(Lean.Grind.not_eq_of_eq_true (eq_true (id (L.cons.inj (id h)).2)))))
|
||
(eq_true h_1))))
|
||
True.intro))
|
||
-/
|
||
#guard_msgs in #print ex3._proof_1_1
|
||
|
||
|
||
-- Check that for numary constructors, we get a trivial inlined “no confusion” principle
|
||
|
||
inductive AlmostEnum where | a | b | mk (b : Bool)
|
||
|
||
-- No explicit noConfusion principle for `AlmostEnum.a`:
|
||
/-- error: Unknown constant `AlmostEnum.a.noConfusion` -/
|
||
#guard_msgs in #print sig AlmostEnum.a.noConfusion
|
||
|
||
|
||
set_option linter.unusedVariables false in
|
||
theorem ex4 (h : AlmostEnum.a = AlmostEnum.a) : True := by
|
||
injection h
|
||
trivial
|
||
|
||
/--
|
||
info: theorem ex4 : AlmostEnum.a = AlmostEnum.a → True :=
|
||
fun h => (fun P => P) True.intro
|
||
-/
|
||
#guard_msgs in #print ex4
|