Possible to prove termination on Type × Prop?

Stream: new members

[aron]

Is it possible to prove that a recursive function terminates through structural recursion on both a Type and Prop?

When I try to put termination_by (expr, ha) in the below code it gives me this error:

Application type mismatch: In the application
  (expr, ha)
the argument
  ha
has type
  TypeOf ctx expr a : Prop
but is expected to have type
  ?m.20208 : Type ?u.20205

My #mwe:

/-- A list which you add items onto at the end -/
inductive Ctx (α : Type u)
  | nil : Ctx α
  | add (body : Ctx α) (tip : α) : Ctx α

inductive PrimLitExpr
  | unit : PrimLitExpr
  | int : Int → PrimLitExpr
  | nat : Nat → PrimLitExpr
  | bool : Bool → PrimLitExpr
  | str : String → PrimLitExpr

inductive Expr : (ctx : Ctx Ty) → Type u where
  | primLit : PrimLitExpr → Expr ctx
  | pair : (fst : Expr ctx) → (snd : Expr ctx) → Expr ctx
  | ife : (cond : Expr ctx) → (ifTrue : Expr ctx) → (ifFalse : Expr ctx) → Expr ctx



inductive PrimTy
  | unit
  | int
  | nat
  | bool
  | str
  deriving DecidableEq

inductive Ty
  | prim : PrimTy → Ty
  | pair : (fst : Ty) → (snd : Ty) → Ty
  | arrow : (from_ : Ty) → (to_ : Ty) → Ty
  deriving DecidableEq


inductive TypeOf : (ctx : Ctx Ty) → (expr : Expr ctx) → (ty : Ty) → Prop where
  | primUnit : TypeOf ctx (Expr.primLit .unit) (Ty.prim .unit)
  | primInt : TypeOf ctx (Expr.primLit (.int _)) (Ty.prim .int)
  | primNat : TypeOf ctx (Expr.primLit (.nat _)) (Ty.prim .nat)
  | primBool : TypeOf ctx (Expr.primLit (.bool _)) (Ty.prim .bool)
  | primStr : TypeOf ctx (Expr.primLit (.str _)) (Ty.prim .str)
  | pair :
    TypeOf ctx fst' fstTy →
    TypeOf ctx snd sndTy →
    TypeOf ctx (.pair fst' snd) (.pair fstTy sndTy)
  | ife :
    TypeOf ctx cond_ (Ty.prim .bool) →
    TypeOf ctx ifTrue t →
    TypeOf ctx ifFalse t →
    TypeOf ctx (Expr.ife cond_ ifTrue ifFalse) t



inductive InferrableType (ctx : Ctx Ty) : (expr : Expr ctx) → Type where
  | inferred : (ty : Ty) → (h : TypeOf ctx expr ty) → InferrableType ctx expr
  | uninferrable : (h : ∀ ty, ¬TypeOf ctx expr ty) → InferrableType ctx expr



/-- The theorem that every expression has a unique type -/
theorem TypeOf.uniqueness {ctx a b} {expr : Expr ctx} (ha : TypeOf ctx expr a) (hb : TypeOf ctx expr b) : a = b := by
  induction ha
  cases hb; rfl
  cases hb; rfl
  cases hb; rfl
  cases hb; rfl
  cases hb; rfl

  case pair ctx exprFst tyFst exprSnd tySnd typeOfFst typeOfSnd hfst hsnd =>
    generalize b = pairType at *
    cases hb with | pair fstHb sndHb =>
      have fstEq := @TypeOf.uniqueness _ _ _ _ typeOfFst fstHb
      have sndEq := @TypeOf.uniqueness _ _ _ _ typeOfSnd sndHb
      simp
      trivial

  case ife ctx exprCond ifTrueExpr ty ifFalseExpr tyCond tyIfTrue tyIfFalse hCond hIfTrue hIfFalse =>
    generalize b = returnTy at *
    cases hb with | ife condHb trueHb falseHb =>
      have fstEq := @TypeOf.uniqueness _ _ _ ifTrueExpr tyIfTrue trueHb
      -- have sndEq := @TypeOf.uniqueness _ _ _ _ tyIfFalse falseHb
      trivial

termination_by (expr,ha)

[aron]

Or is the issue here that Prod.mk only works with Sort 1s and above, i.e. no Props (which have Sort 0)?

Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β

[Aaron Liu]

This will be difficult.

[aron]

can you elaborate?

[Yaël Dillies]

Can you use docs#PProd ?

[aron]

Using docs#PProd gives me a different error:

The termination measure's type must not depend on the function's varying parameters, but TypeOf.uniqueness's termination measure does:
  {ctx : Ctx Ty} →
    {a b : Ty} → {expr : Expr ctx} → TypeOf ctx expr a → TypeOf ctx expr b → Expr ctx ×' TypeOf ctx expr a
Try using `sizeOf` explicitly

[Aaron Liu]

Try this

/-- The theorem that every expression has a unique type -/
theorem TypeOf.uniqueness {ctx a b} {expr : Expr ctx} (ha : TypeOf ctx expr a) (hb : TypeOf ctx expr b) : a = b := by
  induction ha generalizing b with
  | @pair ctx exprFst tyFst exprSnd tySnd typeOfFst typeOfSnd hfst hsnd =>
    cases hb with | pair fstHb sndHb =>
      have fstEq := hfst fstHb
      have sndEq := hsnd sndHb
      rw [fstEq, sndEq]
  | @ife ctx exprCond ifTrueExpr ty ifFalseExpr tyCond tyIfTrue tyIfFalse hCond hIfTrue hIfFalse =>
    cases hb with | ife condHb trueHb falseHb =>
      exact hIfTrue trueHb
  | _ => cases hb; rfl

[aron]

Oh... yeah. How the heck did I miss that :thinking::face_palm: lol

[Aaron Liu]

Generally when doing recursion on Prop-valued objects it's best to avoid termination_by since all proofs of the same proposition are equal, and every pair of proofs of any two propositions are HEq.

[aron]

Ok so the ife case works perfectly when I put that in my code without touching anything else, but now the pair case doesn't work in my code – presumably because the generalizing does some work here. Although I can't quite wrap my head around what it does exactly

[Aaron Liu]

Can you provide a #mwe?

[aron]

all I'm saying is that your solution needs the generalizing b in the induction tactic and it breaks if you remove it

[aron]

but I don't quite understand what it does, because the only effect it has is inside the cases tactic. Before the cases hb with | pair fstHb sndHb => line b is still just b. It only breaks down into fstTy✝.pair sndTy✝ inside cases hb with | pair fstHb sndHb =>. Which seems odd

[Aaron Liu]

generalizing b makes the induction hypothesis universally quantified over all b

[aron]

Btw although this has solved my problem what does this error message actually mean? The termination measure's type must not depend on the function's varying parameters, but inferType's termination measure does?

What is a varying parameter and why should termination measures not depend on them? Surely it should depend on a varying parameter, because if it doesn't vary (shrink) how can you know recursion terminates?