coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Carvalho <hugoccomp AT gmail.com>
- To: t x <txrev319 AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Re: Dependent Type Minimal Example
- Date: Sun, 18 Aug 2013 16:24:05 -0300
I'm not sure about how minimal this is, and the amount of inferences the refine tactic does might still be a bit too much magical, but here's my solution (assuming your change from "destruct" to "induction"):
simpl. rewrite IHexpr. refine (
match (expOpt Nat expr) with
| NConst x => _
| Inc x => _
end);reflexivity.
Also, here's a slightly different formulation, that i did in order to witness just how much was inferred by refine (and also to make a proof term without "ind" functions).
Fixpoint lem' (expr: exp Nat) : expDenote _ (expOpt _ expr) = expDenote _ expr.
refine (
match expr with
| NConst _ => _
| Inc expr' => _
end).
reflexivity.
simpl.
refine (
match (lem' expr') with
| eq_refl => _
end).
refine (
match (expOpt Nat expr') with
| NConst x' => _
| Inc x' => _
end).
reflexivity.
reflexivity.
Qed.
2013/8/18 t x <txrev319 AT gmail.com>
EDIT: last line is meant to be "induction expr; auto" not "destruct expr; auto"On Sun, Aug 18, 2013 at 4:09 PM, t x <txrev319 AT gmail.com> wrote:
Proofs involving dependent types seems to high levels of "black magic" which makes it nearly impossible to debug. I'd like to see a minimal "manual" solution to see what's going on.Hi,Can someone post a minimal solution to this (without using dep_destruct from cpdt tactics) ?
https://gist.github.com/anonymous/6262395
Thanks
- [Coq-Club] Dependent Type Minimal Example, t x, 08/18/2013
- [Coq-Club] Re: Dependent Type Minimal Example, t x, 08/18/2013
- Re: [Coq-Club] Re: Dependent Type Minimal Example, Hugo Carvalho, 08/18/2013
- Re: [Coq-Club] Re: Dependent Type Minimal Example, t x, 08/19/2013
- Re: [Coq-Club] Re: Dependent Type Minimal Example, Hugo Carvalho, 08/18/2013
- Re: [Coq-Club] Dependent Type Minimal Example, Matthieu Sozeau, 08/20/2013
- [Coq-Club] Re: Dependent Type Minimal Example, t x, 08/18/2013
Archive powered by MHonArc 2.6.18.