coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Rui Baptista <rpgcbaptista AT gmail.com>
- To: Adam Chlipala <adamc AT csail.mit.edu>
- Cc: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Fwd: Question about recursion and induction
- Date: Sun, 15 Sep 2013 20:34:49 +0100
Require Import Arith.
Require Import Omega.
Lemma less_subtr : forall n1 n2, n2 <> 0 -> ~ n1 < n2 -> n1 - n2 < n1.
Proof. auto with *. Qed.
Definition div : forall (n1 n2 : nat) (H1 : n2 <> 0), nat.
induction 1 as [n1 div] using (well_founded_induction lt_wf).
apply (
fun n2 H1 =>
match lt_dec n1 n2 with
| left _ => 0
| right H2 => S (div (n1 - n2) (less_subtr _ _ H1 H2) n2 H1)
end).
Defined.
Eval lazy in div 3109 7.
On Sun, Sep 15, 2013 at 7:18 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:
On 09/15/2013 02:07 PM, Ilmārs Cīrulis wrote:I don't think it's a useful exercise to try to work with [Fix] without using [refine]. Almost always, it's a wildly impractical choice to write non-trivial proof terms manually in Coq. Even people who have progressed well beyond beginner status tend to avoid it, and it's not that the experts are applying this arcane, powerful technique and reaping huge rewards. Rather, it's mostly useless.
I want to understand/learn recursion and induction, using Wf.v with its Acc, well_founded, Fix. well_founded_induction.
Accessibility and well-foundedness I have understood, but not very much further.
If it's possible to do only with wf.v and without "refine" then it's the way I need. I'm beginner and want learn this one way. Anything else must wait for later. So - thanks, Rui, but it's not what I need.
I suggest always building proofs using tactics unless you have a really, really good reason not to.
By the way, [refine] is an extremely simple tactic. I don't think there's any reason to try to avoid it here to skip an extra stage of prerequisite understanding. I suggested Chapter 7 of CPDT to introduce general recursion, and Chapter 6 introduces [refine]. It may even be worth going through CPDT from the beginning, accepting that you won't be writing any general-recursive functions until you make your way back to Chapter 7. Coq has a way of confounding your intuitions about what should be easy (and so a good choice for initial explorations) and what should be hard (and so worth putting off until after reading more background).
- [Coq-Club] Question about recursion and induction, Ilmārs Cīrulis, 09/13/2013
- Re: [Coq-Club] Question about recursion and induction, Adam Chlipala, 09/14/2013
- Message not available
- [Coq-Club] Fwd: Question about recursion and induction, Ilmārs Cīrulis, 09/14/2013
- Re: [Coq-Club] Fwd: Question about recursion and induction, Rui Baptista, 09/14/2013
- Re: [Coq-Club] Fwd: Question about recursion and induction, Ilmārs Cīrulis, 09/15/2013
- Re: [Coq-Club] Fwd: Question about recursion and induction, Adam Chlipala, 09/15/2013
- Re: [Coq-Club] Fwd: Question about recursion and induction, Rui Baptista, 09/15/2013
- Re: [Coq-Club] Fwd: Question about recursion and induction, Adam Chlipala, 09/15/2013
- Re: [Coq-Club] Fwd: Question about recursion and induction, Ilmārs Cīrulis, 09/15/2013
- Re: [Coq-Club] Fwd: Question about recursion and induction, Rui Baptista, 09/14/2013
- [Coq-Club] Fwd: Question about recursion and induction, Ilmārs Cīrulis, 09/14/2013
- Message not available
- Re: [Coq-Club] Question about recursion and induction, Adam Chlipala, 09/14/2013
Archive powered by MHonArc 2.6.18.