Search code examples
coqdependent-typecoq-tacticltac

Coq: performing inversion on Prop for Set when there is only one case

Suppose I have some programming language, with a "has type" relation and a "small step" relation.

Inductive type : Set :=
| Nat : type
| Bool : type.

Inductive tm : Set :=
| num : nat -> tm
| plus : tm -> tm -> tm
| lt : tm -> tm -> tm
| ifthen : tm -> tm -> tm -> tm.

Inductive hasType : tm -> type -> Prop :=
| hasTypeNum :
    forall n, hasType (num n) Nat
| hasTypePlus:
    forall tm1 tm2,
      hasType tm1 Nat ->
      hasType tm2 Nat ->
      hasType (plus tm1 tm2) Nat
| hasTypeLt:
    forall tm1 tm2,
      hasType tm1 Nat ->
      hasType tm2 Nat ->
      hasType (lt tm1 tm2) Bool
| hasTypeIfThen:
    forall tm1 tm2 tm3,
      hasType tm1 Bool ->
      hasType tm2 Nat ->
      hasType tm3 Nat ->
      hasType (ifthen tm1 tm2 tm3) Nat.

Inductive SmallStep : tm -> tm -> Prop :=
  ...

Definition is_value (t : tm) := ...

The key detail here is that for each term variant, there's only one possible HasType variant that could possible match.

Suppose then that I want to prove a progress lemma, but that I also want to be able to extract an interpreter from this.

Lemma progress_interp: 
  forall tm t, 
  hasType tm t -> 
  (is_value tm = false) -> 
  {tm2 | SmallStep tm tm2}.
intro; induction tm0; intros; inversion H.

This gives the error Inversion would require case analysis on sort Set which is not allowed for inductive definition hasType.

I understand why it's doing this: inversion performs case analysis on a value of sort Prop, which we can't do since it gets erased in the extracted code.

But, because there's a one-to-one correspondence between the term variants and type derivation rules, we don't actually have to perform any analysis at runtime.

Ideally, I could apply a bunch of lemmas that look like this:

plusInv: forall e t, hasType e t ->
  (forall e1 e2, e = plus e1 e2 -> hasType e1 Nat /\ hasType e2 Nat ).

where there would be a lemma like this for each case (or a single lemma that's a conjunction of these cases).

I've looked at Derive Inversion but it doesn't seem to do what I'm looking for here, though maybe I'm not understanding it correctly.

Is there a way to do this sort of "case analysis where there's only one case?" Or to get the equalities implied by the Prop proof, so that I can only write the possible cases in my extracted interpreter? Can deriving these lemmas be automated, with Ltac or a Deriving mechanism?

Solution

  • Lemma plus_inv can be obtained by a case analysis on type tm instead of a case analysis on type hasType.

    Lemma plus_inv : forall e t, hasType e t ->
  (forall e1 e2, e = plus e1 e2 -> hasType e1 Nat /\ hasType e2 Nat ).
Proof.
intros e; case e; try (intros; discriminate).
intros e1 e2 t h; inversion h; intros e5 e6 heq; inversion heq; subst; auto.
Qed.

    The proof of your main objective progress_interp can probably be performed by induction ont the structure of tm as well. This tantamounts to writing your interpreter directly as a gallina recursive function.

    Your question has a second part: can this be automated. The answer is yes, probably. I suggest using either the template-coq package or the elpi package for this. Both packages are available as opam packages.