How to simplify a proof by induction in Lean?

Question

I'd like to simplify a proof by induction in Lean.

I've defined an inductive type with 3 constructors in Lean and a binary relation on this type. I've included the axioms because Lean wouldn't let me have them as constructors for rel.


inductive Fintype : Type
| a : Fintype
| b : Fintype
| c : Fintype

inductive rel : Fintype → Fintype →  Prop 
| r1 : rel Fintype.a Fintype.b
| r2 : ∀ p : Prop, (p → rel Fintype.a Fintype.c )
| r3 : ∀ p : Prop, (¬ p → rel Fintype.c Fintype.b) 


axiom asymmetry_for_Fintype : ∀ x y : Fintype, rel x y → ¬ rel y x
axiom trivial1 : ¬ rel Fintype.c Fintype.a
axiom trivial2 : ¬ rel Fintype.b Fintype.c
axiom trivial3 : ∀ p : Prop, rel Fintype.a Fintype.c → p 
axiom trivial4 : ∀ p : Prop, rel Fintype.c Fintype.b → ¬ p

A goal was to prove the following theorem:

def nw_o_2 (X : Type) (binrel : X → X → Prop) (x y : X) : Prop := ¬ binrel y x
def pw_o_2 (X : Type) (binrel : X → X → Prop )(x y : X) : Prop := ∀ z : X, (binrel z x → binrel z y) ∧ (binrel y z → binrel x z)

theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=

I've proved it by induction on x, y, and z; the "z" comes from the definition of pw_o_2 above. But the proof is quite long (~136 lines). Is there another way to have a shorter proof?

Can you post your proof online (maybe as Github gist, or pastebin). Are you using term mode or tactic mode? Alternatively, ask the question on leanprover.zulipchat.com for more interaction. — jmc
@jmc I've used tactics. Here's the link to the proof: pastebin.com/VR4H5g10. — LyX2394
You can compress your proof using the all_goals and try and repeat tactics. However, I wouldn't be surprised if you can actually turn it into a one-liner with dec_trivial. You might want to read up on that last one. — jmc
Great! I've reduced the length of the proof to one-fourth of its original length. Thanks. — LyX2394

Rob Lewis Rob Lewis · Accepted Answer · 2019-06-04T07:49:13

Note that your first two axioms are really theorems, provable with an empty pattern match. (The constructors of an inductive types are assumed to be surjective.) The periods at the ends of these lines indicates that the declaration is over, that no body is expected. Internally, Lean is recursing on a proof of rel Fintype.c Fintype.a and showing that each case is structurally impossible.

lemma trivial1 : ¬ rel Fintype.c Fintype.a.
lemma trivial2 : ¬ rel Fintype.b Fintype.c.

Your second two axioms are inconsistent, which makes the proof of your theorem easy but uninteresting.

theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=
false.elim (trivial3 _ (rel.r2 _ trivial))

I'm not sure that you've defined rel in the way you meant to. The second and third constructors are equivalent to just rel Fintype.a Fintype.c and rel Fintype.c Fintype.b respectively.

lemma rel_a_c : rel Fintype.a Fintype.c :=
rel.r2 true trivial

lemma rel_c_b : rel Fintype.c Fintype.b :=
rel.r3 false not_false

How to simplify a proof by induction in Lean?

1 Answers