The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 28 Jul 2013 08:38:38 +0100,
Valentin Robert 
<valentin.robert.42 AT gmail.com>
 a écrit :

> 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

What about:

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

  set (P := fun d => match d as d0 return [[d0]] -> Prop with
                     | natD => fun e => e < 42 | boolD => fun _ => True
  end). change (P natD (eval_term env t)).

  case t; subst P; simpl; auto; clear t; destruct envD; simpl in *.
  unfold vec_ith, hvec_ith, denote_vec, invariant, all_nats in *; simpl
  in *.

  induction x; simpl in *.

  intros [].

  destruct v, env, INV.
  intros [f|]; simpl in *; auto.
  now apply IHx.
Qed.