Structural recursion hint fails

Stream: lean4

[Wojciech Nawrocki]

Hello WfRel experts! I gave Rustan's challenge a shot using a big-step normalization relation. But proofs by structural recursion on derivations of this relation are failing, and I am not entirely sure how to fix them other than by coming up with a manual termination measure based on a data-relevant argument . I would be grateful for tips as to why thesizeOf h < sizeOf h' hint doesn't help.

import Mathlib.Data.Set.Finite
import Mathlib.Tactic.Linarith

abbrev Var := String

inductive Expr where
  | lit : Bool → Expr
  | var : Var → Expr
  | ite : Expr → Expr → Expr → Expr
  deriving DecidableEq, Inhabited

abbrev Env := List (Var × Bool)

namespace Env

instance : Membership (Var × Bool) Env :=
  ⟨fun (x, b) Γ => (x, b) ∈ Γ⟩

def vars : Env → Finset Var :=
  List.foldr (fun (x, _) acc => insert x acc) ∅

@[simp] theorem vars_cons : vars (p :: Γ) = insert p.1 (vars Γ) := by
  simp [vars]

def getVar (Γ : Env) (x : Var) : Option Bool :=
  Γ.find? (·.1 = x) |>.map (·.snd)

end Env

namespace Expr

def tr : Expr := lit true
def fls : Expr := lit false

@[simp] def eval (Γ : Env) : Expr → Option Bool
  | lit b => b
  | var s => Γ.getVar s
  | ite c t f => do
    let cv ← eval Γ c
    if cv then eval Γ t
    else eval Γ f

@[simp] def fv : Expr → Finset Var
  | lit _ => ∅
  | var x => {x}
  | ite c t f => fv c ∪ fv t ∪ fv f

/-- A big-step 'normalizes to' relation `Γ | e ↝ e'`.
The output is guaranteed to be in normal form.
We first verify the correctness of this relation,
and then write a function to compute it. -/
inductive Norm : Env → Expr → Expr → Prop
  | nLit : Norm Γ (lit b) (lit b)
  | nVar : x ∉ Γ.vars → Norm Γ (var x) (var x)
  | nVarMem : (x, b) ∈ Γ → Norm Γ (var x) (lit b)
  | nIteTr : Norm Γ c tr → Norm Γ t t' → Norm Γ (ite c t f) t'
  | nIteFls : Norm Γ c fls → Norm Γ f f' → Norm Γ (ite c t f) f'
  | nIteVarEq :
    Norm Γ c (var x) → Norm ((x, true)::Γ) t t' → Norm ((x, false)::Γ) f f' → t' = f' →
    Norm Γ (ite c t f) t'
  | nIteVarNe :
    Norm Γ c (var x) → Norm ((x, true)::Γ) t t' → Norm ((x, false)::Γ) f f' → t' ≠ f' →
    Norm Γ (ite c t f) (ite (var x) t' f')
  | nIteIteEq :
    Norm Γ c (ite (var x) t' f') → Norm ((x, true)::Γ) (ite t' t f) t'' → Norm ((x, false)::Γ) (ite f' t f) f'' → t'' = f'' →
    Norm Γ (ite c t f) t''
  | nIteIteNe :
    Norm Γ c (ite (var x) t' f') → Norm ((x, true)::Γ) (ite t' t f) t'' → Norm ((x, false)::Γ) (ite f' t f) f'' → t'' ≠ f'' →
    Norm Γ (ite c t f) (ite (var x) t'' f'')

open Norm
local notation Γ " ∣ " e " ↝ " e':30 => Norm Γ e e'

/-- `Nf X e` means that `e` is in normal form and none of its free variables appear in `X`. -/
inductive Nf : Finset Var → Expr → Prop
  | nfLit : Nf X (lit b)
  | nfVar : x ∉ X → Nf X (var x)
  | nfIte : x ∉ X → t ≠ f → Nf (insert x X) t → Nf (insert x X) f → Nf X (ite (var x) t f)
open Nf

theorem Nf.var_subset (hYX : Y ⊆ X) : Nf X e → Nf Y e
  | nfLit => nfLit
  | nfVar hX => nfVar fun hY => hX (hYX hY)
  | nfIte hX hNe h₁ h₂ =>
    nfIte (fun hY => hX (hYX hY)) hNe
      (h₁.var_subset (Y.insert_subset_insert _ hYX))
      (h₂.var_subset (Y.insert_subset_insert _ hYX))

theorem finsetext {A B : Finset α} (x : α) : A = B → (x ∈ A ↔ x ∈ B) :=
  fun h => iff_of_eq (congrArg (Membership.mem x) h)

theorem Nf.disjoint_fv : Nf X e → X ∩ fv e = ∅ := by
  intro h; induction h with
  | nfLit | nfVar => simp [*]
  | nfIte _ _ _ _ ih₁ ih₂ =>
    apply Finset.subset_empty.mp
    intro x h
    have ih₁ := finsetext x ih₁
    have ih₂ := finsetext x ih₂
    simp at h ih₁ ih₂ ⊢
    aesop

theorem Norm.nf : Γ ∣ e ↝ e' → Nf Γ.vars e'
  | nLit | nVarMem _ => nfLit
  | nVar h => nfVar h
  | h'@(nIteTr _ h) | h'@(nIteFls _ h) =>
    have : sizeOf h < sizeOf h' := sorry -- why doesn't this help?
    h.nf
  | nIteVarEq _ he hf h => he.nf.var_subset (by simp [Finset.subset_insert])
  | nIteVarNe hc ht hf h => by
    have hc := hc.nf.disjoint_fv
    have ht := ht.nf
    have hf := hf.nf
    apply nfIte <;> aesop
  | nIteIteEq _ he hf h => he.nf.var_subset (by simp [Finset.subset_insert])
  | nIteIteNe (x := x) hc ht hf h => by
    have hc := finsetext x hc.nf.disjoint_fv
    have ht := ht.nf
    have hf := hf.nf
    apply nfIte <;> aesop
  termination_by nf _ _ _ h => sizeOf h

[Mario Carneiro]

@Wojciech Nawrocki Have you tried proving that have statement? Because it's not true, and the reason simp fails is because the preprocessing reduced the goal to False.

    have : sizeOf h = sizeOf h' := rfl

[Mario Carneiro]

It doesn't work because Γ ∣ e ↝ e', being a proposition, has at most one element and hence its SizeOf instance is trivial

[Mario Carneiro]

The match compiler doesn't understand structural recursion over inductive propositions, but you should be able to write this using the induction tactic instead

[Mario Carneiro]

theorem Norm.nf : Γ ∣ e ↝ e' → Nf Γ.vars e' := by
  intro h; induction h with
  | nLit | nVarMem _ => exact nfLit
  | nVar h => exact nfVar h
  | nIteTr _ h _ ih | nIteFls _ h _ ih => exact ih
  | nIteVarEq _ _ _ _ _ ihf => exact ihf.var_subset (by simp [Finset.subset_insert])
  | nIteVarNe _ _ _ h ihc iht ihf =>
    have hc := ihc.disjoint_fv
    apply nfIte <;> aesop
  | nIteIteEq _ _ _ _ _ ihf => exact ihf.var_subset (by simp [Finset.subset_insert])
  | @nIteIteNe _ _ x _ _ _ _ _ _ _ _ _ h ihc iht ihf =>
    have hc := finsetext x ihc.disjoint_fv
    apply nfIte <;> aesop

[Wojciech Nawrocki]

Ah, false assumption would do it! Of course we can't eliminate Prop into Nat. induction was the first thing I tried, but it gave me a scary error about indices. It works now, however. Thanks!