Termination checker problem for mutual block

Stream: new members

[Vadim Zaliva]

I am hitting a problem with the termination checker on a relatively simple example: https://gist.github.com/vzaliva/df21596578211d99d7aa5d2699fec46b. The error "Cannot derive unfold equation beqExpr._mutual.eq_def
Tactic simp failed with a nested error: (deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached". I've tried increasing maxHeartbeats, but it didn't help. I manually provided the termination measure and proofs for all functions in the block, but it still did not help. Any suggestions on how to fix that?

[Aaron Liu]

seems to work fine if you do structural recursion

import Std.Data.HashMap
import Mathlib.Tactic
open Std

abbrev Address := Nat
abbrev Name := String

inductive Typ : Type where
  | int : Typ
  | bool : Typ
  | unit : Typ
  | ref : Typ → Typ
  | arrow : Typ → Typ → Typ
  | string : Typ
  deriving Repr, DecidableEq

def Typ.beq : Typ → Typ → Bool
  | int, int => true
  | bool, bool => true
  | unit, unit => true
  | string, string => true
  | ref t1, ref t2 => Typ.beq t1 t2
  | arrow t1 t2, arrow t1' t2' => Typ.beq t1 t1' && Typ.beq t2 t2'
  | _, _ => false

instance : BEq Typ where
  beq := Typ.beq

inductive Op : Type where
  | add : Op
  | sub : Op
  | mul : Op
  | div : Op
  | gte : Op
  | lte : Op
  | gt  : Op
  | lt  : Op
  | eq  : Op
  | and : Op
  | bitand : Op
  | or  : Op
  | neq : Op
  deriving Repr, BEq, DecidableEq

inductive UnaryOp : Type where
  | not : UnaryOp
  deriving Repr, BEq, DecidableEq

abbrev Tag := Nat

inductive EffectTarget where
  | namedVar : Name → EffectTarget
  | returnValue : EffectTarget
  deriving Repr, BEq

mutual

inductive SyntaxPredicate : Type where
  | guardClosure: Tag → Name → Expr → SyntaxPredicate
  | guardOnly : Tag → SyntaxPredicate
  | noPred : SyntaxPredicate

structure Effect where
  target : EffectTarget
  poison : Bool
  pred : SyntaxPredicate

inductive ExternReturn where
  | simple : Typ → Bool → SyntaxPredicate → ExternReturn
  | nestedFn : Name → Typ → ExternReturn → List Effect → ExternReturn
  | nestedPfn : Name → Typ → ExternReturn → ExternReturn

inductive Expr : Type where
  | unit : Expr
  | num : Int → Expr
  | bool : Bool → Expr
  | str : String -> Expr
  | var : Name → Expr
  | op : Expr → Op → Expr → Expr
  | unaryop :  UnaryOp → Expr → Expr
  | ite : Expr → Expr → Expr → Expr
  | newRef : Expr → Expr
  | assign : Expr → Expr → Expr
  | deref : Expr → Expr
  | seq : Expr → Expr → Expr
  | kwhile : Expr → Expr → Expr
  | vlet : Name → Expr → Expr → Expr
  | fn : Name → Typ → Expr → Typ → Expr
  | pfn : Name → Typ → Expr → Typ → Expr
  | app : Expr → Expr → Expr
  | rand  : Expr -> Expr
  | frand : Expr -> Expr
  | printString  : Expr -> Expr
  | printInt  : Expr -> Expr
  | externVal : Typ → Bool → SyntaxPredicate → Expr
  | externFn : Name → Typ → ExternReturn → List Effect → Expr
  | externPfn : Name → Typ → ExternReturn → Expr

end

mutual

def beqExpr : Expr → Expr → Bool
  | Expr.unit, Expr.unit => true
  | Expr.num n1, Expr.num n2 => n1 == n2
  | Expr.bool b1, Expr.bool b2 => b1 == b2
  | Expr.str s1 , Expr.str s2 => s1 == s2
  | Expr.var x1, Expr.var x2 => x1 == x2
  | Expr.op e1 op1 e2, Expr.op e1' op2 e2' => beqExpr e1 e1' && op1 == op2 && beqExpr e2 e2'
  | Expr.unaryop op1 e1, Expr.unaryop op2 e2 => op1 == op2 && beqExpr e1 e2
  | Expr.ite e1 e2 e3, Expr.ite e1' e2' e3' => beqExpr e1 e1' && beqExpr e2 e2' && beqExpr e3 e3'
  | Expr.newRef e1, Expr.newRef e2 => beqExpr e1 e2
  | Expr.assign e1 e2, Expr.assign e1' e2' => beqExpr e1 e1' && beqExpr e2 e2'
  | Expr.deref e1, Expr.deref e2 => beqExpr e1 e2
  | Expr.seq e1 e2, Expr.seq e1' e2' => beqExpr e1 e1' && beqExpr e2 e2'
  | Expr.kwhile e1 e2, Expr.kwhile e1' e2' => beqExpr e1 e1' && beqExpr e2 e2'
  | Expr.vlet x1 e1 e2, Expr.vlet x2 e1' e2' => x1 == x2 && beqExpr e1 e1' && beqExpr e2 e2'
  | Expr.fn x1 t1 e1 t1', Expr.fn x2 t2 e2 t2' => x1 == x2 && t1 == t2 && beqExpr e1 e2 && t1' == t2'
  | Expr.pfn x1 t1 e1 t1', Expr.pfn x2 t2 e2 t2' => x1 == x2 && t1 == t2 && beqExpr e1 e2 && t1' == t2'
  | Expr.app e1 e2, Expr.app e1' e2' => beqExpr e1 e1' && beqExpr e2 e2'
  | Expr.rand e1, Expr.rand e2 => beqExpr e1 e2
  | Expr.frand e1, Expr.frand e2 => beqExpr e1 e2
  | Expr.printString e1, Expr.printString e2 => beqExpr e1 e2
  | Expr.printInt e1, Expr.printInt e2 => beqExpr e1 e2
  | Expr.externVal t1 p1 pred1, Expr.externVal t2 p2 pred2 =>
      t1 == t2 && p1 == p2 && beqSyntaxPredicate pred1 pred2
  | Expr.externFn x1 t1 ret1 eff1, Expr.externFn x2 t2 ret2 eff2 =>
      x1 == x2 && t1 == t2 && beqExternReturn ret1 ret2 && beqEffectList eff1 eff2
  | Expr.externPfn x1 t1 ret1, Expr.externPfn x2 t2 ret2 =>
      x1 == x2 && t1 == t2 && beqExternReturn ret1 ret2
  | _, _ => false
termination_by structural e1 _ => e1

def beqSyntaxPredicate : SyntaxPredicate → SyntaxPredicate → Bool
  | SyntaxPredicate.guardClosure k1 arg1 body1, SyntaxPredicate.guardClosure k2 arg2 body2 =>
      k1 == k2 && arg1 == arg2 && beqExpr body1 body2
  | SyntaxPredicate.guardOnly k1, SyntaxPredicate.guardOnly k2 => k1 == k2
  | SyntaxPredicate.noPred, SyntaxPredicate.noPred => true
  | _, _ => false
termination_by structural p1 _ => p1

def beqEffect : Effect → Effect → Bool
  | ⟨t1, p1, pred1⟩, ⟨t2, p2, pred2⟩ =>
      t1 == t2 && p1 == p2 && beqSyntaxPredicate pred1 pred2
termination_by structural ef1 _ => ef1

def beqEffectList : List Effect → List Effect → Bool
  | [], [] => true
  | e1 :: es1, e2 :: es2 => beqEffect e1 e2 && beqEffectList es1 es2
  | _, _ => false
termination_by structural efs1 _=> efs1

def beqExternReturn : ExternReturn → ExternReturn → Bool
  | ExternReturn.simple t1 p1 pred1, ExternReturn.simple t2 p2 pred2 =>
      t1 == t2 && p1 == p2 && beqSyntaxPredicate pred1 pred2
  | ExternReturn.nestedFn x1 t1 ret1 eff1, ExternReturn.nestedFn x2 t2 ret2 eff2 =>
      x1 == x2 && t1 == t2 && beqExternReturn ret1 ret2 && beqEffectList eff1 eff2
  | ExternReturn.nestedPfn x1 t1 ret1, ExternReturn.nestedPfn x2 t2 ret2 =>
      x1 == x2 && t1 == t2 && beqExternReturn ret1 ret2
  | _, _ => false
termination_by structural r1 _ => r1

end

[Vadim Zaliva]

That worked! Thanks @Aaron Liu !