## Stream: new members

### Topic: induction: "argument 2 not a variable"

#### Sarah Mameche (Jan 03 2019 at 21:11):

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 (Jan 03 2019 at 21:40):

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 (Jan 03 2019 at 21:49):

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 (Jan 03 2019 at 21:54):

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 (Jan 03 2019 at 22:02):

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

#### Rob Lewis (Jan 03 2019 at 22:03):

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

#### Sarah Mameche (Jan 03 2019 at 22:09):

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

#### Kevin Buzzard (Jan 03 2019 at 23:12):

I guess most people here use 3.4.1.

#### Sarah Mameche (Jan 03 2019 at 23:26):

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 (Jan 04 2019 at 03:42):

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

Last updated: May 13 2021 at 20:13 UTC