The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Hello club,

Standalone code here: http://paste.awesom.eu/Ptival/sJU&ln

The gist of my problem is as follows. I defined a typed language of
terms, similar to this:

Inductive term : desc -> Type :=
| NatLit (n: nat) : n < 42 -> term natD
| BoolLit : bool -> term boolD
| Var (i: fin (projT1 envD)) : term (vec_ith envD i)
.

Each base type has a description (natD denotes nat, boolD denotes bool).
Every term is indexed by the description of its type.
In particular, Vars index safely into an environment whose description
is a vector of base descriptions.
Notice the silly requirement that natural literal numbers are bounded by 42.

A simple evaluator is defined as (an environment env of description
envD is in the section's scope):

Definition eval_term (d: desc) (t: term d) : [[d]] :=
  match t with
  | NatLit n _ => n
  | BoolLit b => b
  | Var i => hvec_ith (existT denote envD env) i
  end.

It guaranteedly returns a value of the expected type.
I set to prove that a certain property is always true for all natural
numbers resulting from an evaluation, knowing it is true for natural
literals, and true for all natural numbers living in my current
environment:

Definition invariant (envD: vec desc) (env: [[envD]]) :=
  all_nats (fun n => n < 42) envD env.

Theorem ok :
  forall (envD: vec desc) (env: [[envD]]) (t: term envD natD),
    invariant envD env ->
    eval_term env t < 42.

In the proof of this theorem, given in the linked URL, I eventually
reached this state:

  ============================
   match vec_ith envD i as _d return (term envD _d -> Prop) with
   | natD => fun tin : term envD natD => eval_term env tin < 42
   | boolD => fun _ : term envD boolD => True
   end (Var envD i)

At that point, I am unable to continue using Coq tactics.

I cannot abstract over (vec_ith envD i) because it makes the
application with (Var envD i) ill-typed.

I cannot generalize (Var envD i) because its concrete value is needed
to compute eval_term after the match.

What I do in the proof is write my own dependent pattern match,
allowing me to shove (Var envD i) inside eval_term, having carefully
wrapped it inside a type cast.

  ============================
   forall EQ : vec_ith envD i = natD,
   eval_term env
     match EQ in (_ = __vi) return (term envD __vi) with
     | eq_refl => Var envD i
     end < 42

From then on, I manage to push eval_term inside the cast, perform the
beta reduction, and prove the remaining goal using my hypotheses.

I find these parts of the proof very cumbersome and brittle: in my
example, the language is much more involved, and writing this big
"refine" is unsatisfactory.

Is there a more clever way to address this (ll. 166-195 in the given link)?

I hope to turn this example into a blog post explaining how inversions
can become complicated (and the infamous "Abstracting over ... leads
to a term ... which is ill-typed"), and I would like to display good
solutions, if possible! (with all credits due if you provide one)

Comments much appreciated!

Best regards,
- Valentin