Zulip Chat Archive

Stream: new members

Topic: Possible to not generalize in cases?

aron (Jun 07 2025 at 15:26):

I am using a cases tactic inside of a proof block where I need to show a contradiction. Before the cases I have:

ifTrueTy : Ty
ifTrueProof : TypeOf ctx ifTrue ifTrueTy
ifFalseTy : Ty
ifFalseProof : TypeOf ctx ifFalse ifFalseTy
hbranches : ¬ifTrueTy = ifFalseTy

But inside the ife case I have:

ifTrueTy : Ty
ifTrueProof✝ : TypeOf ctx ifTrue ifTrueTy
ifFalseTy : Ty
ifFalseProof✝ : TypeOf ctx ifFalse ifFalseTy
ifTrueProof : TypeOf ctx ifTrue ty
ifFalseProof : TypeOf ctx ifFalse ty
hbranches : ¬ifTrueTy = ifFalseTy

In other words, the *Proofs get overridden by a version that replaces the last type index with ty. But I can only prove that there is a contradiction if I can show that ifTrueTy = ty and ifFalseTy = ty. But since cases doesn't let me show that ifTrueProof = ifTrueProof✝ I can't do that.

How can I link overridden variables to the new ones that have replaced them?

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
  | 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)
  | 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


mutual

def inferType (ctx : Ctx Ty) (expr : Expr ctx) : InferrableType ctx expr :=
  match h : expr with
  | .ife cond ifTrue ifFalse =>
    have condDecidable : Decidable _ := TypeOf.decidable ctx cond (.prim .bool)

    have ifTrueInferred := inferType ctx ifTrue
    have ifFalseInferred := inferType ctx ifFalse

    match condDecidable, ifTrueInferred, ifFalseInferred with
    | .isTrue condProof, .inferred ifTrueTy ifTrueProof, .inferred ifFalseTy ifFalseProof =>
      if hbranches : ifTrueTy = ifFalseTy then
        .inferred _ (TypeOf.ife condProof ifTrueProof (hbranches ▸ ifFalseProof))
      else
        by
        refine .uninferrable ?_
        intro ty hh
        cases hh with
        | ife condProof ifTrueProof ifFalseProof =>
          -- How can I prove that `ifTrueProof = ifTrueProof✝` and `ifFalseProof = ifFalseProof✝`?
          contradiction


def TypeOf.decidable (ctx : Ctx Ty) (expr : Expr ctx) (ty : Ty) : Decidable (TypeOf ctx expr ty) :=
  match hexpr : expr, hty : ty with
  | .primLit .unit, .prim .unit => .isTrue TypeOf.primUnit
  | .primLit (.int _), .prim .int => .isTrue TypeOf.primInt
  | .primLit (.nat _), .prim .nat => .isTrue TypeOf.primNat
  | .primLit (.bool _), .prim .bool => .isTrue TypeOf.primBool
  | .primLit (.str _), .prim .str => .isTrue TypeOf.primStr

end

Eric Wieser (Jun 07 2025 at 16:21):

If you do

       | ife condProof ifTrueProof' ifFalseProof' =>
          have : ifTrueProof' = ifTrueProof := rfl

you'll see the the statement isn't even well-typed

aron (Jun 07 2025 at 18:13):

hm yeah but uhh... how come? ifTrueTy and ty both have type Ty so I don't understand how they don't have the same type?

aron (Jun 07 2025 at 18:16):

hm ok I don't think that's the real issue because if I do have a hypothesis that ifTrueTy = ty then it type checks just fine

have : ifTrueTy = ty := by sorry
have : ifTrueProof' = (this ▸ ifTrueProof) := by rfl

aron (Jun 07 2025 at 18:33):

Ok I managed to prove the thing but I don't know how it worked. I did:

        exact
        match hh with
        | .ife condProof ifTrueProof ifFalseProof =>
          by
          have : ty = ifTrueTy := by exact _
          rw [← this] at hbranches
          have : ty = ifFalseTy := by exact _
          rw [← this] at hbranches
          contradiction

Full working code

Is there any way to see what terms Lean used to auto-fill holes? Because I'd love to know how it knew that ty = ifTrueTy and ty = ifFalseTy

Eric Wieser (Jun 07 2025 at 18:35):

Lean is not filling the holes at all, it's too busy complaining that your match is incomplete.

Eric Wieser (Jun 07 2025 at 18:35):

You need to add sorry branches to the match to get a useful error

aron (Jun 07 2025 at 18:37):

oh. that's disappointing. alright so i guess my initial question still stands.

aron (Jun 07 2025 at 18:56):

hm actually I think my question was wrong. Because cases is not replacing the original ifTrueTy and ifFalseTy at all... ty comes from the new hypothesis that I am creating by using intro ty hh which is that if ifTrueTy ≠ ifFalseTy then there exists no type ty for which a TypeOf ctx expr ty can be constructed... but I don't think I can prove that with the code I have. I think for that I need to have a theorem that proves that each expression can only have one type, something like

theorem TypeOf.uniqueness {ctx a b} {expr : Expr ctx} (ha : TypeOf ctx expr a) (hb : TypeOf ctx expr b) : a = b

otherwise even though I've shown that ifTrueTy ≠ ifFalseTy, that will only let me prove ¬TypeOf ctx expr ifTrueTy, but not that there is no possible type for expr: ∀ ty, ¬TypeOf ctx expr ty

Last updated: Dec 20 2025 at 21:32 UTC