Skip to Content.
Sympa Menu

coq-club - [Coq-Club] functional induction, Equations plugin

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] functional induction, Equations plugin


Chronological Thread 
  • 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 *)





Archive powered by MHonArc 2.6.18.

Top of Page