The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thank you!

This is amazing, worked on multiple (simple + complicated) examples I had with dependent types.

==================

I have a really dumb question now:

Why do standard texts deal with all the guess work of:

  pattern _blah_;

  generalize dependent _blah_;

  apply dep_destruct;

  intros;

  generalize ...

  refine (UIP_refl ... );

where incorrect guesses gives back compiler complaints that abstracting Foo over Bar results in ill-typed form ...

The "refine" technique seems to be a silver bullet. Are there cases where "refine" fails, but manually generalizing / UIP_refl-ing terms makes things work?

On Sun, Aug 18, 2013 at 7:24 PM, Hugo Carvalho <hugoccomp AT gmail.com> wrote:

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:

Hi,

  Can someone post a minimal solution to this (without using dep_destruct from cpdt tactics) ?

  https://gist.github.com/anonymous/6262395

  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.

Thanks