The Coq mailing list

[Feró <ferenc.tamasi AT gmail.com>]

By unfolding expDenote & cfold, then using dependent destruction it's
quite straightforward.

Require Import Program.
Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold 
e).
Proof.
  induction e; auto; unfold expDenote at 1; fold @expDenote; unfold
cfold; fold @cfold;
  try first [
        (* ternaries *)
        rewrite IHe1, IHe2, IHe3;
        remember (cfold e1) as cfe1;
        remember (cfold e2) as cfe2;
        remember (cfold e3) as cfe3;
        dependent destruction cfe1;
        dependent destruction cfe2;
        dependent destruction cfe3;
        simpl; first [ reflexivity | destruct b; simpl; reflexivity ]
      | (* binaries *)
        rewrite IHe1, IHe2;
        remember (cfold e1) as cfe1;
        remember (cfold e2) as cfe2;
        dependent destruction cfe1;
        dependent destruction cfe2;
        simpl; reflexivity
      | (* unaries *)
        rewrite IHe;
        remember (cfold e) as cfe;
        dependent destruction cfe;
        simpl; reflexivity
      ].
Qed.

On Sun, Jul 6, 2014 at 8:22 PM, Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 wrote:
> Hi all,
>
> I'm reading CPDT(Certified Programming with Dependent Types) and I'm
> typing all the code in the book and following through proofs. I don't
> like the book's approach of using magical and non-standard proof
> tactics so I'm manually proving parts that are proved using `crush`
> and similar tactics.
>
> It worked mostly fine since I already had basics grasped thanks to
> SF(Software Foundations) but now I'm stuck with "dependent destruct"
> parts, which I see for the first time.
>
> I pasted the code here http://lpaste.net/107016 . I'm looking for
> proving that last theorem without using magical CPDT proofs. I'd like
> to go with only standard tactics/definitions. Can anyone give me some
> tips on how to approach this proof? At least some keywords to do some
> research would be appreciated.
>
> Thanks.
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net



-- 
Give me liberty or give me cash!