Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

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.