induction for Prop-valued predicates

Stream: lean4

[Kat Zhuchko]

I am having trouble understanding how induction for Prop-valued inductive predicates
works. This is a small MWE, where Lean complains about termination to prove a simple
statement by induction, in the SimSym case of SimCong_inj:

inductive Tree where
  | Leaf : Nat → Tree
  | Plus : Tree → Tree → Tree
open Tree

inductive Sim : Tree → Tree → Prop where
  | SimCong : Sim a b
            → Sim (Plus a q) (Plus b q)
  | SimRfl : Sim R R
  | SimSym : Sim R₁ R₂ → Sim R₂ R₁
open Sim

theorem SimCong_inj (h : Sim (Plus a q) (Plus b q)) :
     Sim a b :=
  match h with
  | Sim.SimCong h => h
  | Sim.SimRfl => Sim.SimRfl
  | Sim.SimSym h₁ =>
    Sim.SimSym (SimCong_inj h₁)

I have then tried using induction instead of match statement, but to no avail: the inductive hypothesis given by induction does not have a usable shape and using generalizing does not
work either.

Does anyone have any hint on how to deal with this?

theorem SimCong_inj'
     (e1 : w1 = (Plus a q))
     (e2 : w2 = (Plus b q))
     (h : Sim w1 w2) :
     Sim a b := by
  induction h with
  | SimCong h ih =>
    simp at e1;
    let ⟨q1,q2⟩ := e1;
    simp at e2;
    let ⟨q3,q4⟩ := e2;
    subst q1 q2
    subst q3
    exact h
  | SimRfl =>
    subst e1
    simp at e2
    subst e2
    exact Sim.SimRfl
  | SimSym h ih =>
    sorry

(Style comments on the proof are also welcome! :smiling_face_with_hearts:)

[Chris Bailey]

The error message is quite dense, but I'm surprised how well it was able to identify the problem.

Not considering parameter h of SimCong_inj:
  its type Sim is an inductive family and indices are not variables
    Sim (a.Plus q) (b.Plus q)

So apparently it can figure it out if you make the indices variables:

theorem SimCong_inj (x y : Tree) (h : Sim x y) (h0 : x = Tree.Plus a q) (h1 : y = Tree.Plus b q):
     Sim a b :=
  match h with
  | @Sim.SimCong a' b' q' h => by
    have ⟨h2, _⟩ := Plus.injEq a' q' a q ▸ h0
    have ⟨h3, _⟩ := Plus.injEq b' q' b q ▸ h1
    rwa [h2, h3] at h
  | Sim.SimRfl => by
    rw [h0] at h1
    have ⟨h2, _⟩ := Plus.injEq a q b q ▸ h1
    rw [h2]
    exact Sim.SimRfl
  | Sim.SimSym h₁ =>
    Sim.SimSym (SimCong_inj y x h₁ h1 h0)

With the way your prop is defined, SimSym is tricky. It seems to be implied by the other two constructors without changing inj. Is it acceptable to just derive it as a theorem? It should make these kinds of proofs easier.

inductive Tree where
  | Leaf : Nat → Tree
  | Plus : Tree → Tree → Tree
open Tree

inductive Sim : Tree → Tree → Prop where
  | SimCong : Sim a b → Sim (Plus a q) (Plus b q)
  | SimRfl : Sim R R
open Sim

theorem SimCong_sym {a b : Tree} : Sim a b → Sim b a
  | SimCong h2 => Sim.SimCong (SimCong_sym h2)
  | SimRfl => Sim.SimRfl

theorem SimCong_inj (a b q : Tree) : Sim (Plus a q) (Plus b q) → Sim a b
  | SimCong h2 =>  h2
  | SimRfl => Sim.SimRfl

[Chris Bailey]

I didn't read your inj' proof carefully, you already figured out the indices thing. When there are equality hypotheses about e.g. w1 = Plus a q, you almost always (in my experience) want to put them after the major premise (the thing you're doing induction/cases on) and not before it. In older versions it had to do with shifting those extra pieces of evidence into the motive so that they're not fixed, now I'm not sure how it gets elaborated tbh.

This particular proof seems brittle, it's accepted on 4.11.0-rc2 but not on 4.10.0

[Kat Zhuchko]

Removing SimSym isn't really an option because of the larger context from which this MWE was coming from... after updating to 4.11.0-rc2 now the match version with indices works, thanks! The version I updated from was 4.7.0, where match+indices was still not working. I'm not really sure why it shouldn't work with non-indices variables during the induction though... Even under 4.11.0-rc2 the induction hypothesis is unusable.