Would you use a Prop or a Type?

Stream: new members

[Dan Plyukhin]

I'm working on mechanizing a lambda calculus. I have inductive types for the syntax:

mutual
  inductive Expr where ...
  inductive Val where ...
  inductive Ty where ...
end

The static semantics is defined by a typing relation, which is currently a Prop:

inductive Typed : Typing.Context -> Expr -> Ty -> Prop where ...

I have a lot of recursive definitions that tell me some property about a typed expression:

def foo: (M: Expr) -> (exists G T, Typed G M T) -> A := ...
def bar: (M: Expr) -> (exists G T, Typed G M T) -> B := ...
def qux: (M: Expr) -> (exists G T, Typed G M T) -> C := ...

But recursive calls are a huge pain, because I have to re-convince Lean that the subexpressions are typed.

def foo (M: Expr) -> (exists G T, Typed G M T) -> A :=
  | (app M1 M2), M_typed =>
    let a1 := foo M1 (... convince Lean that M1 is typed ...)
    let a2 := foo M2 (... convince Lean that M2 is typed ...)
    ...

How would you change things to make foo and bar and qux easier to define? My main idea is to change Typed from a Prop to a Type and so I could just write something like def foo : Typed M -> A = ... but I'm worried this could somehow bite me later in the project. For example, you can't use the cases tactic on a Type.

[Dan Plyukhin]

Err, now I realize converting it to a Type wouldn't be enough because there are still a G and a T getting existentially quantified. That is, I couldn't define def foo : (exists G T, Typed G M T) -> A because foo's argument would be a Prop. I guess I could use PSigma instead. But surely there's a simpler way?

[Edward van de Meent]

you might ask for G and T to be provided explicitly to foo?

[Dan Plyukhin]

True! But I'd still have to construct a new G and T when I make recursive calls to foo, right? Ideally I could just write:

let a1 := foo M1
let a2 := foo M2
...

[Edward van de Meent]

could be... although maybe that's where you can write some lemmas to help?

[Edward van de Meent]

if you use the "exists G T" version, you'd need to provide a proof of this anyway

[Edward van de Meent]

btw you can use the cases tactic on a value of a type. for example:

example (n : Nat) : Or (n = 0) (exists (n':Nat), n = n' + 1) := by
  cases n
  . simp only [Nat.self_eq_add_left, Nat.add_one_ne_zero, exists_const, or_false]
  . simp only [Nat.add_one_ne_zero, Nat.add_right_cancel_iff, exists_eq', or_true]

[Kyle Miller]

In case it's helpful as a case study, in docs#Rack.PreEnvelGroupRel' I found it was easier to make a Type-valued relation for recursion purposes, and then I "propified" it in docs#Rack.PreEnvelGroupRel (That's the same as using Nonempty; I don't remember why it is a custom type.)

[Edward van de Meent]

readability?

[Edward van de Meent]

naming?

[Edward van de Meent]

there can be many good reasons

[Kyle Miller]

Good guesses, but we'll never know. I wrote it, and I don't remember ;-)

[Dan Plyukhin]

@Edward I think that sounds similar to what I have already---for each typing rule in Typed, I have inversion lemmas that tell me the subexpressions are typed. Something like:

lemma app_inv1 G M1 M2 T : Typed G (app M1 M2) T -> (exists G T, Typed M1 T) := ...
lemma app_inv2 G M1 M2 T : Typed G (app M1 M2) T -> (exists G T, Typed M2 T) := ...

So my definition of foo can go something like this:

def foo (M: Expr) -> (exists G T, Typed G M T) -> A :=
  | (app M1 M2), M_typed =>
    let a1 := foo M1 (by app_inv1)
    let a2 := foo M2 (by app_inv2)
    ...

It's minimal, but still tedious

[Dan Plyukhin]

@Kyle ooh cool idea!

[Edward van de Meent]

depending on how you define Typed, since you're doing matching, you could maybe recover these values from just matching on M_typed?

[Dan Plyukhin]

Assuming Typed is a Type right? Because we can't match on a Prop at runtime IIRC

[Dan Plyukhin]

In that case indeed the inversion lemmas could just be replaced with getters on M_typed

[Dan Plyukhin]

Well, I'd still have to pack the proof together with witness context and type

[Edward van de Meent]

yea, i don't think youll be able to avoid that

[MrQubo]

Maybe something like that could work?

structure Typed where
  M : Expr
  T : Ty
  proof : exists G, M.isOfType T := by is_of_type_tactic
attribute [simp] Typed.proof

You would have to work out good tactic, but assuming it worked, you can construct Typed just by providing Expr and Ty.