coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cédric <sedrikov AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A better way to address a tricky inversion?
- Date: Sun, 28 Jul 2013 17:11:06 +0200
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.
- [Coq-Club] A better way to address a tricky inversion?, Valentin Robert, 07/28/2013
- Re: [Coq-Club] A better way to address a tricky inversion?, AUGER Cédric, 07/28/2013
- Re: [Coq-Club] A better way to address a tricky inversion?, Valentin Robert, 07/28/2013
- Re: [Coq-Club] A better way to address a tricky inversion?, AUGER Cédric, 07/28/2013
Archive powered by MHonArc 2.6.18.