Recovering information about one term by induction on o...

Stream: new members

[Dan Plyukhin]

I have an inductive datatype for expressions,

  inductive Exp : Type where
    | app (M₁ : Exp) (M₂ : Exp)
    | ...

and one for type derivations:

inductive Typed : Context → Exp → Ty → Type where
  | app:
    Typed Γ M₁ (funTy T1 T2) →
    Typed Γ M₂ T1→
    --------------------------------
    Typed Γ (app M₁ M₂) T2

I'm trying to prove a proposition by induction on type derivations of expressions. I'll elide the details and show the important bit:

example (M_typed : Typed Γ M T) : False := by
  induction M_typed with
  | app h1 h2 ih1 ih2 =>
    admit

Since the app typing rule only holds when M is app, I would expect to find an equation in my context telling me that M = app ?M1 ?M2. But I don't! Instead my context shows no relationship between M and the type derivation:

Γ : Context
M : Exp
T : Ty
Γ✝ : Context
M₁✝ : Exp
T₁✝ T₂✝ : Ty
M₂✝ : Exp
h1 : Typed Γ✝ M₁✝ (T₁✝.funType T₂✝)
h2 : Typed Γ✝ M₂✝ T₁✝
ih1 ih2 : False
⊢ False

How do I recover the fact that M = app M₁✝ M₂✝?

[Aaron Liu]

Why do you need this? If induction has worked correctly, there should be no mention of M in your environment anymore, so even if you knew this, you would not be able to do anything with it.

[Aaron Liu]

You can do generalize hM : M = M' at M_typed; induction M_typed generalizing M with ... (not tested, because you didn't post a #mwe)

[Dan Plyukhin]

Hmm good point! I want it because the app typing rule has a ton of implicit arguments (Gamma, T1, T2, M1, M2, and other rules have even more implicit arguments). I need to give names to M1 and M2, and I don't want to give names to the other arguments. I could just use underscores:

induction M_typed with
| @app _ _ M₁ M₂ _ _ h1 h2 ih1 ih2 =>

but that doesn't look very nice. I like your idea of using generalize! I'll try that.

[Notification Bot]

Dan Plyukhin has marked this topic as resolved.

[Notification Bot]

Dan Plyukhin has marked this topic as unresolved.

[Dan Plyukhin]

I went down the generalize rabbit hole, and I didn't like what I saw :) I've constructed an MWE in case anybody has other ideas.

The code below shows a simply typed lambda calculus, and an attempt to prove a proposition by induction on the type derivation. In that proof, I know M must have the form app M1 M2, and I want to give names to that M1 and M2. So my question is, what's the cleanest way to do that?

import Mathlib.Data.Finmap

def Var := String
  deriving DecidableEq

inductive Exp where
  | app (M₁ : Exp) (M₂ : Exp)
  | var (x : Var)

inductive Ty : Type where
  | funType (T₁ T₂ : Ty)
  | basicType

open Exp Ty

abbrev Typing.Context := Finmap (λ _ : Var ↦ Ty)

inductive Typed : Typing.Context → Exp → Ty → Type where
  | app {Γ M₁ M₂ T₁ T₂} :
    Typed Γ M₁ (funType T₁ T₂) →
    Typed Γ M₂ T₁ →
    --------------------------------
    Typed Γ (app M₁ M₂) T₂

  | var {Γ x T} :
    Γ.lookup x = some T →
    ----------------------
    Typed Γ (var x) T

example {M_typed : Typed Γ M T} : M = M := by
  induction M_typed with
  | app M₁_ty M₂_ty ih₁ ih₂ =>
    let (app M₁ M₂) := M               -- PROBLEM: The typechecker doesn't accept this!
    admit
  | var h =>
    admit

[Aaron Liu]

Come up with a better mwe?

example {M_typed : Typed Γ M T} : M = M := by
  induction M_typed with
  | app M₁_ty M₂_ty ih₁ ih₂ =>
    clear M -- `clear`ly, you don't need `M`
    rename_i M₁ M₂ _ _
    sorry
  | var h =>
    sorry

[Dan Plyukhin]

:skull: We can forget about M since I can just define let M:= app M1 M2. I don’t like rename_i because it’s not robust to change. If I mess around with other parts of the proof or add parameters to Typed.app, then rename_i breaks.

[Aaron Liu]

This is the case for other tactics too, right? If I add a constructor or reorder the arguments to Typed.app, the induction breaks too.

[Dan Plyukhin]

If I add a constructor I expect things to break. Ideally I want my automation to be robust enough that I can reorder arguments and most proofs wouldn’t break.