Unable to figure the term when destructing an inductive proposition

[fduxiao]

I defined a simple type and a simple relation.

inductive Three: Type where
  | a | b | c

inductive Rel3: Three -> Three -> Prop where
  | ab: Rel3 a b
  | cb: Rel3 c b

Rel3 is obviously transitive.

theorem rel3_trans: forall {x y z: Three}, Rel3 x y -> Rel3 y z -> Rel3 x z := sorry

I tried to prove it. But lean failed to figure out the correct term if you destruct some of type Rel3 x y

theorem rel3_trans: forall {x y z: Three}, Rel3 x y -> Rel3 y z -> Rel3 x z := by
  intros x y z Hxy Hyz
  cases Hxy
  case ab =>
    -- Here in case ab, Hyz should be `Rel3 b z`, but lean sticked to `Rel3 y z`.
    -- And, you are unable to destruct `Hyz` again by `cases Hyz`
    admit
  case cb =>
    admit

If you use cases Hyz in the above, lean will complain that tactic 'induction' failed, major premise type is not an inductive type.

Meanwhile, you can prove this in Coq.

Inductive Three :=
  | a | b | c.

Inductive Rel3: Three -> Three -> Prop :=
  | ab: Rel3 a b
  | cb: Rel3 c b.


Theorem rel3_trans: forall x y z: Three, Rel3 x y -> Rel3 y z -> Rel3 x z.
Proof.
  intros x y z Hxz Hyz.
  destruct Hxz.
  - destruct Hyz.
    + apply ab.
    + apply ab.
  - destruct Hyz.
    + apply cb.
    + apply cb.
Qed.

Am I using the correct strategy to prove that? In lean, how do you prove it?

[fduxiao]

What about this one even simpler?

inductive T: Type where
  | a | b

inductive R: T -> T -> Prop where
  | r: R a b

example: Not (R b a) := by
  intros H
  cases H
  admit

[digama0]

Questions of this nature are better suited for the Zulip, please use issues on this repo only to report actual issues in lean.

The error in your code is that a and b in Rel3 are being interpreted as variables, not elements of Three, because they are namespaced as Three.a and Three.b, so you can either write that or use .a and .b in the definition of Rel3. If you would like to avoid the implicit introduction of a and b as variables, you should use set_option autoImplicit true or add it as a global setting in the lakefile.

inductive Three: Type where
  | a | b | c

inductive Rel3: Three -> Three -> Prop where
  | ab: Rel3 .a .b
  | cb: Rel3 .c .b

theorem rel3_trans: forall {x y z: Three}, Rel3 x y -> Rel3 y z -> Rel3 x z := by
  intros x y z Hxy Hyz
  cases Hxy <;> cases Hyz