The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi t x,

  This problem doesn't require equality reasoning, just inversion of Exp nat
which is readily defined from the dependent eliminator for exp.

Definition exp_nat_e (P : exp Nat -> Type)
         (p0 : forall n, P (NConst n))
         (pinc : forall e, P e -> P (Inc e)) : forall {e}, P e :=
  exp_rect (fun t e => 
              match t return exp t -> Type with
                | Nat => P 
                | Bool => fun e => True 
              end e)
           p0 pinc Nat.
              
Lemma expDInc e :
  expDenote Nat (expOpt Nat (Inc e)) = S (expDenote Nat (expOpt Nat e)).
Proof.
  simpl expOpt at 1. generalize (expOpt Nat e). clear e.
  refine (@exp_nat_e _ _ _); simpl; auto.
Qed.

Lemma lem:
  forall (expr: exp Nat),
    expDenote _ expr = expDenote _ (expOpt _ expr).
Proof.
  refine (@exp_nat_e _ _ _); [auto|].
  simpl expDenote at 3. intros e ->. auto using expDInc.
Qed.


On 18 août 2013, at 18:09, 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