Rewriting things inside ifs?

Stream: new members

[Guilherme Espada]

In this example:

example : (if (0<1) then 1 else 2) = 1 := begin
  have proof: ((0:int)<(1:int))=true := by sorry,
  rw proof,
end

I don't see why the rewrite shouldn't work. What am I missing? What is a good way to handle ifs (both in the conclusion and in the premises)?

Thanks

[Eric Wieser]

Well for one, your theorem statement is about nat, but proof is about int

[Eric Wieser]

simp_rw proof works after you fix that

[Guilherme Espada]

Oh, simp_rw seems exactly what I was looking for. Another tool for my toolbelt.

Why doesn't rw behave like simp_rw?

[Mario Carneiro]

Because the condition of an if statement has a dependent argument, the proof that this condition is decidable, that needs to be rewritten as well

[Mario Carneiro]

rw doesn't handle this very well, it gives a motive is not type correct error in these cases

[Guilherme Espada]

Mario Carneiro said:

rw doesn't handle this very well, it gives a motive is not type correct error in these cases

That's exactly the error I was seeing when experimenting. Couldn't really understand it unfortunately

[Guilherme Espada]

Thank you both for your answers :smile:

[Mario Carneiro]

simp_rw has the same interface as rw but uses the proof strategy of simp, which is able to handle dependencies in some places (but may sometimes fail to rewrite where rw will work)

[Guilherme Espada]

Something weird is happening: simp_rw works correctly in the example posted above, and in another minimized example which I extracted with extract_goal:

import tactic.suggest
import data.finset
import data.finmap
import data.list
import data.finmap

@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype

open ttype


instance : inhabited ttype := inhabited.mk ty_bool

@[derive decidable_eq]
inductive term
|t_var (idx:int) : term
|t_abs (T:ttype) (t:term) : term
|t_app (t1 t2: term) : term
|t_true : term
|t_false : term
|t_if (cond l r: term): term

open term

instance : inhabited term := inhabited.mk t_true

def upshift_cutoff : int → int → term → term
| d c (t_var k) := t_var (if (k<c) then k else (k + d))
| d c (t_abs T t) := t_abs T $ upshift_cutoff d (c+1) t
| d c (t_app t1 t2) := t_app (upshift_cutoff d c t1) (upshift_cutoff d c t2)
| d c t_true := t_true
| d c t_false := t_false
| d c (t_if cond l r) := t_if (upshift_cutoff d c cond) (upshift_cutoff d c l) (upshift_cutoff d c r)

def upshift (amt:int) (t1:term): term := upshift_cutoff amt 0 t1

def subst  : int → term → term → term
| idx s (t_var n) := if n = idx then s else t_var n
| idx s (t_abs T t) := t_abs T $ (subst (idx+1) (upshift 1 s) t)
| idx s (t_app t1 t2) := t_app (subst idx s t1) (subst idx s t2)
| idx s t_true := t_true
| idx s t_false := t_false
| idx s (t_if cond l r) := t_if (subst idx s cond) (subst idx s l) (subst idx s r)

inductive eval : term → term → Prop
| e_app1 {t1 t1' t2} : eval t1 t1' → eval (t_app t1 t2) (t_app t1' t2)
| e_app2 {t1 t2 t2'} : eval t2 t2' → eval (t_app t1 t2) (t_app t1 t2')
| e_appabs {T11 t12 v2} : eval (t_app (t_abs T11 t12) v2) (upshift (-1) (subst 0 (upshift 1 v2) t12))
| e_if_true {t2 t3} : eval (t_if t_true t2 t3) (t2)
| e_if_false {t2 t3} : eval (t_if t_false t2 t3) (t3)
| e_if {t1 t1' t2 t3} : eval t1 t1' → eval (t_if t1 t2 t3) (t_if t1' t2 t3)

example
  (b : eval
         ((t_abs ty_bool (t_abs ty_bool (t_var 0))).t_app (t_true.t_app t_true))
         (t_abs ty_bool (t_var (ite (0 < 1) 0 (-1))))) (kk : 0 < 1 = true) :
  eval ((t_abs ty_bool (t_abs ty_bool (t_var 0))).t_app (t_true.t_app t_true))
    (t_abs ty_bool (t_var 0)) :=
begin
  simp_rw kk at b, --works as expected
  simp at b,
  assumption,
end

However, in the more complex example I'm actually trying to prove, with the same context and goal as the example I posted above, it fails with simplify tactic failed to simplify (apologies for the huge example, but minification makes the issue disappear):

import tactic.suggest
import data.finset
import data.finmap
import data.list
import data.finmap
import tactic.linarith

@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype

open ttype


instance : inhabited ttype := inhabited.mk ty_bool

@[derive decidable_eq]
inductive term
|t_var (idx:int) : term
|t_abs (T:ttype) (t:term) : term
|t_app (t1 t2: term) : term
|t_true : term
|t_false : term
|t_if (cond l r: term): term

open term

instance : inhabited term := inhabited.mk t_true

def upshift_cutoff : int → int → term → term
| d c (t_var k) := t_var (if (k<c) then k else (k + d))
| d c (t_abs T t) := t_abs T $ upshift_cutoff d (c+1) t
| d c (t_app t1 t2) := t_app (upshift_cutoff d c t1) (upshift_cutoff d c t2)
| d c t_true := t_true
| d c t_false := t_false
| d c (t_if cond l r) := t_if (upshift_cutoff d c cond) (upshift_cutoff d c l) (upshift_cutoff d c r)

def upshift (amt:int) (t1:term): term := upshift_cutoff amt 0 t1

def subst  : int → term → term → term
| idx s (t_var n) := if n = idx then s else t_var n
| idx s (t_abs T t) := t_abs T $ (subst (idx+1) (upshift 1 s) t)
| idx s (t_app t1 t2) := t_app (subst idx s t1) (subst idx s t2)
| idx s t_true := t_true
| idx s t_false := t_false
| idx s (t_if cond l r) := t_if (subst idx s cond) (subst idx s l) (subst idx s r)

inductive eval : term → term → Prop
| e_app1 {t1 t1' t2} : eval t1 t1' → eval (t_app t1 t2) (t_app t1' t2)
| e_app2 {t1 t2 t2'} : eval t2 t2' → eval (t_app t1 t2) (t_app t1 t2')
| e_appabs {T11 t12 v2} : eval (t_app (t_abs T11 t12) v2) (upshift (-1) (subst 0 (upshift 1 v2) t12))
| e_if_true {t2 t3} : eval (t_if t_true t2 t3) (t2)
| e_if_false {t2 t3} : eval (t_if t_false t2 t3) (t3)
| e_if {t1 t1' t2 t3} : eval t1 t1' → eval (t_if t1 t2 t3) (t_if t1' t2 t3)

abbreviation ctxtype := list ttype

def lookup_list : ctxtype → int → option ttype
| (head :: tail) 0  := some head
| (head :: tail) n  := lookup_list tail (n-1)
| list.nil _ := none
@[simp]
def in_ctx (idx: int) (val: ttype) (ctx:ctxtype) := lookup_list ctx idx = (some val)

inductive typ : ctxtype → term → ttype → Prop
| typ_var {ctx x T} : x≥0 → in_ctx x T ctx → typ ctx (t_var x) T
| typ_abs {ctx T1 t2 T2} : typ (T1::ctx) t2 T2 → typ ctx (t_abs T1 t2) (ty_func T1 T2)
| typ_app {ctx t1 T11 T12 t2} : (typ ctx t1 (ty_func T11 T12)) → (typ ctx t2 T11) → typ ctx (t_app t1 t2) T12
| typ_true {ctx} : typ ctx t_true ty_bool
| typ_false {ctx} : typ ctx t_true ty_bool
| typ_if {ctx cond l r T} : typ ctx cond ty_bool -> typ ctx l T -> typ ctx r T  -> typ ctx (t_if cond l r) T

open typ

theorem subject_expansion_fails : ¬ (∀ ctx t t' T, typ ctx t' T → eval t t' → typ ctx t T) :=
begin
  simp,
  existsi (∅:ctxtype),
  existsi t_app (t_abs ty_bool (t_abs ty_bool (t_var 0))) (t_app t_true t_true),
  existsi t_abs  ty_bool (t_var 0),
  existsi ty_func ty_bool ty_bool,
  split,
  {
    refine typ_abs _,
    refine typ_var _ rfl,
    linarith,
  },
  split,
  {
    have a:= eval.e_appabs,
    have b: eval (t_app (t_abs ty_bool (t_abs ty_bool (t_var 0))) (t_true.t_app t_true)) (upshift (-1) (subst 0 (t_true.t_app t_true)  (t_abs ty_bool (t_var 0)))) := a,


    repeat{
      rw subst at b <|>
      rw upshift at b <|>
      rw upshift_cutoff at b <|>
      simp at b
    },
    have kk: (0<1)=true := by sorry,
    simp_rw kk at b, --error here


    rw subst at b,
    simp at b,
    rw upshift_cutoff at b,
    rw upshift_cutoff at b,
    exact b,
  },
  {
    intro a,
    cases a,
    cases a_ᾰ,
    cases a_ᾰ,
    cases a_ᾰ_1,
    cases a_ᾰ_1_ᾰ,
  }
end

[Guilherme Espada]

I can workaround the bug by extracting to a lemma and using that, but this behavior seems weird to me

[Kevin Buzzard]

Your mistake can be easily spotted if you use the infoview in VS code (and if you know what to look for -- this is a common slip ;-) ) and has nothing to do with Lean weirdness. Clicking on the 0 < 1 within the ite shows that it's an inequality of integers, and clicking on the one on kk shows that it's an inequality of naturals. So you can fix with

    have kk: ((0 : ℤ) <1)=true := by sorry,
    simp_rw kk at b, -- works

[Kevin Buzzard]

PS have kk: ((0 : ℤ) <1)=true := by simp [zero_lt_one],

[Kevin Buzzard]

PPS the whole point of introducing those weird hard-to-type ᾰ characters was to encourage users to name their own variables, users aren't supposed to be putting them in code.

[Guilherme Espada]

Thanks for the help. I have another question: Why does the behavior differ when I extract the lemma? Does lean automatically try to figure out the right kind of 0 somehow, which differs when the lemma is extracted?

Regarding ᾰ, I'm trying to avoid it in new code. However, I have a large file that used autogenerated names (back when they used to be a) and it isn't really practical for me to rewrite it all.

[Kevin Buzzard]

Yes, Lean has a "figure out which zero it is" thing going on, it's called typeclass resolution applied to the class has_zero.zero. However, in contrast to most other pieces of notation, numerals have this "default type" of nat. Some of us would love to see the back of this, and if we had our way then your version of kk would simply fail with the error "I don't know which 0 you're talking about". But I think the designers had their reasons for this default to nat thing. All I see is the confusion it causes ;-)

[Johan Commelin]

Guilherme Espada said:

Regarding ᾰ, I'm trying to avoid it in new code. However, I have a large file that used autogenerated names (back when they used to be a) and it isn't really practical for me to rewrite it all.

Is it practical for you to downgrade to an older version of lean? Or do you need the newest version of mathlib?

[Guilherme Espada]

Not really, the version I was using before had a bunch of broken things in visual studio. Besides, I really don't mind having to use ᾰ every now and then for old proofs, and I already went through and replaced the as with ᾰ where needed. So at this point, I really wouldn't gain anything from downgrading.