coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] well founded induction computation

From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
To: Thery Laurent <thery AT ns.di.univaq.it>
Cc: rouxcody AT loria.fr, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] well founded induction computation
Date: Thu, 13 Nov 2008 13:32:43 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thery Laurent wrote:

What is happening here? Otherwise I completely agree that programming by proof as I have done is quite disadvisable.

The problem is your two subst in your wf_fix.
Unfortunately, rewriting in dependent types makes you lose
reduction.

--
Laurent Théry

Actually, it would not make you loose reduction if the proofs you are rewriting with were transparent enough to be reducible to refl_equal...

Yves

[Coq-Club] well founded induction computation, rouxcody
- Re: [Coq-Club] well founded induction computation, Thery Laurent
  - Re: [Coq-Club] well founded induction computation, Yves Bertot