The Coq mailing list

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

I see, so the idea is:

- Destructing t in the context "eval_term t < 42" is not going to
work, because the context is ill-typed for other concrete indices than
t's one.
- So we can replace the goal with "P d (eval_term t)", such that "P
natD (eval_term t)" reduces to the current goal, and "P d (eval_term
t)" reduces to something trivial for other indices.
- In the context "P d (eval_term t)" it is fine to destruct t. We
successfully turned ill-typed goals into vacuous goals.

So really, my first step could have been:

  dependent inversion_clear t with (fun d t =>
    match d as _d return [[_d]] -> Prop with
    | natD => fun v => v < 42
    | _ => fun _ => True
    end (eval_term env t)
  ).

which turns in two goals easily solved.

Thanks for the help!

- Valentin

On Sun, Jul 28, 2013 at 4:11 PM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> 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.