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?
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.