diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/subtac/test/id.v | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/subtac/test/id.v')
-rw-r--r-- | contrib/subtac/test/id.v | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/contrib/subtac/test/id.v b/contrib/subtac/test/id.v new file mode 100644 index 00000000..9ae11088 --- /dev/null +++ b/contrib/subtac/test/id.v @@ -0,0 +1,46 @@ +Require Coq.Arith.Arith. + +Require Import Coq.subtac.Utils. +Program Fixpoint id (n : nat) : { x : nat | x = n } := + match n with + | O => O + | S p => S (id p) + end. +intros ; auto. + +pose (subset_simpl (id p)). +simpl in e. +unfold p0. +rewrite e. +auto. +Defined. + +Check id. +Print id. +Extraction id. + +Axiom le_gt_dec : forall n m, { n <= m } + { n > m }. +Require Import Omega. + +Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } := + if le_gt_dec n 0 then 0 + else S (id_if (pred n)). +intros. +auto with arith. +intros. +pose (subset_simpl (id_if (pred n))). +simpl in e. +rewrite e. +induction n ; auto with arith. +Defined. + +Print id_if_instance. +Extraction id_if_instance. + +Notation "( x & y )" := (@existS _ _ x y) : core_scope. + +Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} := + (a & a). +intros. +auto. +Qed. |