coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gert Smolka <smolka AT ps.uni-saarland.de>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] functional induction, Equations plugin
- Date: Sun, 25 Nov 2012 13:53:53 +0100
I wonder why functional induction doesn't work even for
simple examples like gcd (see below). Would the Equations
plugin perform any better?
- Gert
Require Import Recdef Omega.
Definition gcd_order (p : nat * nat) : nat := let (x,y) := p in x+y.
Function gcd (p : nat * nat) {measure gcd_order p} : nat :=
match p with
| (0,_) => 0
| (_,0) => 0
| (x,y) => match gt_eq_gt_dec x y with
| inleft (left _) => gcd (x, y-x)
| inleft (right _) => x
| inright xgty => gcd (x-y, y)
end
end.
- unfold gcd_order ; intros ; omega.
- unfold gcd_order ; intros ; omega.
Defined.
Lemma gcd_ref x y :
x=y -> gcd (x,y) = x.
Proof.
functional induction (gcd(x,y)).
- (* Already the first case is unprovable *)
- [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Julien Forest, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Matthieu Sozeau, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Message not available
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Pierre Courtieu, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Matthieu Sozeau, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Julien Forest, 11/25/2012
Archive powered by MHonArc 2.6.18.