From 17550e80aa0c7fbeaec13d46629c92de6967b1d1 Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 2 Sep 2008 21:36:06 +0000 Subject: Add support for recursive definitions to [Equations], deciding if a definition is recursive or not based on occurence of a rec call in the body. Examples updated, enjoy! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11353 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/Equations.v | 29 +++++++++++------------------ 1 file changed, 11 insertions(+), 18 deletions(-) (limited to 'test-suite') diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v index d08ce884c..3ef591959 100644 --- a/test-suite/success/Equations.v +++ b/test-suite/success/Equations.v @@ -6,7 +6,7 @@ Obligation Tactic := try equations. Equations neg (b : bool) : bool := neg true := false ; neg false := true. - + Eval compute in neg. Require Import Coq.Lists.List. @@ -27,20 +27,13 @@ Eval compute in (tail _ (cons 1 nil)). Equations app' {A} (l l' : list A) : (list A) := app' A nil l := l ; -app' A (cons a v) l := cons a (app v l). +app' A (cons a v) l := cons a (app' A v l). Eval compute in app'. -Fixpoint zip {A} (f : A -> A -> A) (l l' : list A) : list A := - match l, l' with - | nil, nil => nil - | cons a v, cons b v' => cons (f a b) (zip f v v') - | _, _ => nil - end. - Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) := zip' A f nil nil := nil ; -zip' A f (cons a v) (cons b w) := cons (f a b) (zip f v w) ; +zip' A f (cons a v) (cons b w) := cons (f a b) (zip' _ f v w) ; zip' A f nil (cons b w) := nil ; zip' A f (cons a v) nil := nil. @@ -50,7 +43,7 @@ Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] be Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) := zip'' A f nil nil def := nil ; -zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip f v w) ; +zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' _ f v w def) ; zip'' A f nil (cons b w) def := def ; zip'' A f (cons a v) nil def := def. @@ -64,15 +57,15 @@ Equations vhead A n (v : vector A (S n)) : A := vhead A n (Vcons a v) := a. Eval compute in (vhead _ _ (Vcons 2 (Vcons 1 Vnil))). - -Axiom cheat : Π A, A. +Eval compute in vhead. Equations vmap {A B} (f : A -> B) n (v : vector A n) : (vector B n) := vmap A B f 0 Vnil := Vnil ; -vmap A B f (S n) (Vcons a v) := Vcons (f a) (cheat _). +vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap A B f n v). Eval compute in (vmap _ _ id _ (@Vnil nat)). Eval compute in (vmap _ _ id _ (@Vcons nat 2 _ Vnil)). +Eval compute in vmap. Inductive fin : nat -> Set := | fz : Π {n}, fin (S n) @@ -86,13 +79,12 @@ Implicit Arguments finle [[n]]. Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := trans (S n) fz j k leqz q := leqz ; -trans (S n) (fs i) (fs j) fz (leqs p) q :=! q ; -trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (cheat _). +trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans _ _ _ _ p q). Lemma trans_eq1 n (j k : fin (S n)) q : trans (S n) fz j k leqz q = leqz. Proof. intros. simplify_equations ; reflexivity. Qed. -Lemma trans_eq2 n i j k p q : trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (cheat _). +Lemma trans_eq2 n i j k p q : trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans _ _ _ _ p q). Proof. intros. simplify_equations ; reflexivity. Qed. Section Image. @@ -106,4 +98,5 @@ Section Image. Eval compute in inv. -End Image. \ No newline at end of file +End Image. + -- cgit v1.2.3