induction: "argument 2 not a variable"

Stream: new members

[Sarah Mameche]

Hi, I have an inductive predicate SN that takes a relation as argument (here eval), see the code snippet below. An induction over the statement SN eval stgives me the error: induction tactic failed, argument #2 of major premise type SN eval st is not a variable.

Is it a problem that SN takes eval as an argument?

inductive tm  : nat -> Type
  | app : Π {ntm : nat}, tm ntm -> tm ntm -> tm ntm
  /- ... -/

reserve infixl `≻`:40
inductive eval : Π {n}, tm n → tm n → Prop
infixl `≻` := eval
| eappl {n} {e₁ : tm n} {e₁' e₂} : e₁ ≻ e₁' →  tm.app e₁ e₂ ≻ tm.app e₁' e₂
  /- ... -/
infix `≻` := eval
open eval

inductive SN {n} : (tm n -> tm n -> Prop) → tm n -> Prop
| sn_step (R: tm n → tm n → Prop) (e1 : tm n) : (forall e2, R e1 e2 -> SN R e2) -> SN R e1.

definition SNe {n} := @SN n eval.

theorem SN₁ {n} (s t : tm n) : SNe (tm.app s t) → SNe s ∧ SNe t :=
begin
  intro h₁, split,
  { generalize h₂ : (tm.app s t) = st, revert h₁, rw h₂, intro h₁, revert s t h₂,
  induction h₁ with st hst ihst,  }

[Rob Lewis]

I get a different error on this example, generalize tactic failed, failed to find expression in the target, which is solved by unfolding SNe at h1. Is this the right code snippet?

[Sarah Mameche]

Oh, I still get the induction error (on the example alone)...
Unfolding SNe at h1 makes the induction tactic work, but gives me this induction hypothesis:
ih_1 : ∀ (e2 : tm n) (a_1 : R e1 e2), (λ (_x : tm n → tm n → Prop) (st : tm n) (h₁ : SN _x st), ∀ (s t : tm n), app s t = st → SNe s) R e2 _

where R is added to the hypotheses, R : tm n → tm n → Prop. I want Rto be eval, though. How can that be done?

[Rob Lewis]

Can you make R a parameter to SN? (Move it to the left of the colon in the definition of SN, that is.)

[Sarah Mameche]

That produces the same induction hypothesis (but unfolding SNe is not needed anymore)

[Rob Lewis]

I think we're either using different versions of Lean, or working on different examples.

[Sarah Mameche]

Ok, maybe my version is too old, I'm using 3-3-0

[Kevin Buzzard]

I guess most people here use 3.4.1.

[Sarah Mameche]

Yeah sorry, I switched versions now and the tip with Ras parameter works for the induction tactic. But there are problems for cases and constructorwith this definiton, for example:

inductive tm  : nat -> Type
  | app : Π {ntm : nat}, tm ntm -> tm ntm -> tm ntm
  /- ... -/

reserve infixl `≻`:40
inductive eval : Π {n}, tm n → tm n → Prop
infixl `≻` := eval
| eappl {n} {e₁ : tm n} {e₁' e₂} : e₁ ≻ e₁' →  tm.app e₁ e₂ ≻ tm.app e₁' e₂
  /- ... -/
infix `≻` := eval
open eval
inductive star {n} (R : tm n → tm n → Prop) : tm n → (tm n → Prop)
| srefl {e} : star e e
| sstep {e₁ e₂ e₃} :  (R e₁ e₂) → star e₂ e₃ → star e₁ e₃
open star
infix `≻*`:40 := star eval

inductive SN {n} (R : tm n -> tm n -> Prop ) : tm n -> Prop
| sn_step (R: tm n → tm n → Prop) (e1 : tm n) : (forall e2, R e1 e2 -> SN e2) -> SN e1.

definition SNe {n} := @SN n eval.

lemma closed_star {n} (s t): s ≻* t -> SNe s -> @SNe n t :=
begin intros h1 h2,  induction h1 with s' s' t' e h3 h4 ih,
      { assumption },
      { apply ih, cases h2,   },
end

Cases adds a hypothesis of type R : tm n → tm n → Prop (similar to what happened with induction before)

[Mario Carneiro]

you have R in the sn_step constructor even though it's already declared, so it's a different R