Induction over RTC

Stream: Program verification

[Andrew]

Hi! I am writing a program logic that defines small-step semantics as follows:

abbrev Configuration := Command × Stack × Trace
inductive small_step : Configuration -> Configuration -> Prop
...

I define a reflexive transitive closure over the small step like this:

inductive rtc (r : α → α → Prop) : α -> α → Prop
| refl (x : α) : rtc r x x
| step (x y z : α) : r x y -> rtc r y z → rtc r x z

def small_step_rtc := rtc small_step

Now, I have a hypothesis of the form:

(skip, σ, τ) ⇝* (skip, σ', τ')

where ⇝* is the small-step reflexive transitive closure. But when I try to perform an induction on this hypothesis, I get:

Invalid target: Index in target's type is not a variable (consider using the `cases` tactic instead)
  (skip, σ, τ)

Is there any way to do this induction without this error? I have tried generalizing and rewriting away my triples, but this is an enormous hassle. Given that I will have to do many inductions of this form, it seems insane to me that I will have to use a workaround for a very simple use-case

[Malvin Gattinger]

There is docs#Relation.ReflTransGen in mathlib, coming with several useful lemmas and induction principles like docs#Relation.ReflTransGen.head_induction_on that you can use with induction some_rtc_hyp using Relation.ReflTransGen.head_induction_on. Maybe use that or have a look how those are proven? (And in my own project here in Pdl.Star are some more lemmas about it.)

An #mwe in one code block that workds in the live-lean browser thingy would be good to help you better.

[Andrew]

Unfortunately the ReflTransGen is in the wrong order (I'm looking for R a b -> RTC R b c -> R a c whereas ReflTransGen does RTC R a b -> R b c -> RTC R a c)

[Andrew]

I'm currently loking over how to use head_induction_on

[Andrew]

This is the #mwe if you'd care to have a look. It seems to be a known limitation of lean that you can't do induction on tuples https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0AZCAc2AGMcAlAU3RWAgDsAoRgE0oDM4BnAVxDgBccAHIo4AdZFiAtAD4pMRgB84ACiQAaOFgCUcALzykcANTbm6SiBDH2ECIO581m7Xv1P+qrFqR65cABiSOhclIIeWACejHBwwPQwUBBccKix8fQsPCQwdPRpcISU9JRQIcAAXgmEcMZYGVzQUFFAA

[Malvin Gattinger]

What would the induction proof here be in English? Why do you want induction in the first place? The sum type here is not inductive, i.e. it does not have values that contain values of the sum type itself, right?

[Aaron Liu]

Andrew said:

Unfortunately the ReflTransGen is in the wrong order (I'm looking for R a b -> RTC R b c -> R a c whereas ReflTransGen does RTC R a b -> R b c -> RTC R a c)

that's a theorem

[Aaron Liu]

Andrew said:

It seems to be a known limitation of lean that you can't do induction on tuples

this feels false

[Andrew]

Malvin Gattinger said:

What would the induction proof here be in English? Why do you want induction in the first place? The sum type here is not inductive, i.e. it does not have values that contain values of the sum type itself, right?

This example doesn't have anything to do with what I'm actually doing, it just surfaces the error I'm running into

[Malvin Gattinger]

Can you give us a more realistic example then? The lemma here seems false because sum (1,2) = sum (2,1) right? And have you tried using cases instead?

[Andrew]

I can't use cases, because in this example I need the inductive hypothesis

[Andrew]

It genuinely doesn't matter what I'm doing, i just need to be able to do an induction in which the hypothesis contains a tuple

[Aaron Liu]

I will need more context

[Andrew]

If you see the error in the #mwe, I'm just trying to get the induction tactic to not fail

[Aaron Liu]

induction on tuples is complicated and it depends on what kind of induction hypotheses you need and whether you are inducting on Props or Types

[Aaron Liu]

Andrew said:

If you see the error in the #mwe, I'm just trying to get the induction tactic to not fail

not sure what you want to accomplish here

[Andrew]

So in my example what I have is a triple:

hstep : (skip, σ, τ) ⇝* (skip, σ', τ')

[Aaron Liu]

your goal is false and there aren't any inductive hypotheses

[Andrew]

Here skip is a constant and sigma and tau are variables

[Aaron Liu]

oh I see

[Andrew]

What I want is to just get induction hstep to go through

[Aaron Liu]

I would do generalize ha : (skip, σ, τ) = a, hb : (skip, σ', τ') = b at hstep followed by induction hstep generalizing ... for a sufficient amount of generalizing

[Aaron Liu]

it really depends on what you want the induction hypothesis to look like

[Andrew]

Yeah so that was my original question

[Andrew]

What I currently have is this:

  generalize hπ : (skip, σ, τ) = π
  generalize hπ' : (skip, σ', τ') = π'
  rw [hπ, hπ'] at hstep
  induction hstep

[Malvin Gattinger]

import Mathlib.Logic.Relation

def Command : Type := sorry
def Stack : Type := sorry
def Trace : Type := sorry

abbrev Configuration := Command × Stack × Trace

def small_step : Configuration -> Configuration -> Prop := sorry

def big_step := Relation.ReflTransGen small_step

def isNice : Configuration → Prop := sorry

theorem something (h : big_step a b ) : isNice b := by
  induction h
  case refl =>
    sorry
  case tail IH =>
    sorry

theorem something_head (h : big_step a b ) : isNice b := by
  induction h using Relation.ReflTransGen.head_induction_on
  case refl =>
    sorry
  case head IH =>
    sorry

[Andrew]

I'm trying to figure out if there's either an idiomatic or less repetitive way of doing this

[Aaron Liu]

yeah I have nothing

[Andrew]

Thanks for the support both of you

[Andrew]

Malvin Gattinger said:

import Mathlib.Logic.Relation

def Command : Type := sorry
def Stack : Type := sorry
def Trace : Type := sorry

abbrev Configuration := Command × Stack × Trace

def small_step : Configuration -> Configuration -> Prop := sorry

def big_step := Relation.ReflTransGen small_step

def isNice : Configuration → Prop := sorry

theorem something (h : big_step a b ) : isNice b := by
  induction h
  case refl =>
    sorry
  case tail IH =>
    sorry

theorem something_head (h : big_step a b ) : isNice b := by
  induction h using Relation.ReflTransGen.head_induction_on
  case refl =>
    sorry
  case head IH =>
    sorry

Im going to see if I can refactor my proof to make this work

[Andrew]

Aaron Liu said:

Andrew said:

Unfortunately the ReflTransGen is in the wrong order (I'm looking for R a b -> RTC R b c -> R a c whereas ReflTransGen does RTC R a b -> R b c -> RTC R a c)

that's a theorem

Can you point me at any way to make the RTC work in the order I want? I'd like to use the Mathlib one if at all possible

[Aaron Liu]

docs#Relation.ReflTransGen.head is the theorem

[Malvin Gattinger]

In my example above please place the cursor after case head IH =>and look at the info view :)

[Aaron Liu]

there's also docs#Relation.ReflTransGen.trans and docs#Relation.ReflTransGen.single

[Aaron Liu]

there's a lot of theorems

[Andrew]

Thanks

[Andrew]

That's a huge help

[Aaron Liu]

you're probably better off looking them up on your own rather than having me list them off