From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/success/ProgramWf.v | 99 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 99 insertions(+)
 create mode 100644 test-suite/success/ProgramWf.v

(limited to 'test-suite/success/ProgramWf.v')

diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
new file mode 100644
index 00000000..81bdbc29
--- /dev/null
+++ b/test-suite/success/ProgramWf.v
@@ -0,0 +1,99 @@
+Require Import Arith Program.
+Require Import ZArith Zwf.
+
+Set Implicit Arguments.
+(* Set Printing All. *)
+Print sigT_rect.
+Obligation Tactic := program_simplify ; auto with *.
+About MR.
+
+Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
+  match n with
+    | 0 => 0
+    | S n' => merge n' m
+  end.
+
+Print merge.
+
+
+Print Zlt.
+Print Zwf.
+
+Open Local Scope Z_scope.
+
+Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z :=
+  match n ?= m with
+    | Lt => Zwfrec n (Zpred m)
+    | _ => 0
+  end.
+
+Next Obligation.
+  red. Admitted.
+
+Close Scope Z_scope.
+
+Program Fixpoint merge_wf (n m : nat) {wf lt m} : nat :=
+  match n with
+    | 0 => 0
+    | S n' => merge n' m
+  end.
+
+Print merge_wf.
+
+Program Fixpoint merge_one (n : nat) {measure n} : nat :=
+  match n with
+    | 0 => 0
+    | S n' => merge_one n'
+  end.
+
+Print Hint well_founded.
+Print merge_one. Eval cbv delta [merge_one] beta zeta in merge_one.
+
+Import WfExtensionality.
+
+Lemma merge_unfold n m : merge n m =
+  match n with
+    | 0 => 0
+    | S n' => merge n' m
+  end.
+Proof. intros. unfold merge at 1. unfold merge_func. 
+  unfold_sub merge (merge n m).
+  simpl. destruct n ; reflexivity. 
+Qed.
+
+Print merge.
+
+Require Import Arith.
+Unset Implicit Arguments.
+
+Time Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
+  (H : forall (i : { i | i < n }), i < p -> P i = true)
+  {measure (n - p)} :
+  Exc (forall (p : { i | i < n}), P p = true) :=
+  match le_lt_dec n p with
+  | left _ => value _
+  | right cmp =>
+      if dec (P p) then
+        check_n n P (S p) _
+      else
+        error
+  end.
+
+Require Import Omega Setoid.
+
+Next Obligation.
+  intros ; simpl in *. apply H.
+  simpl in * ; omega.
+Qed.
+
+Next Obligation. simpl in *; intros.
+  revert H0 ; clear_subset_proofs. intros.
+  case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst.
+  revert H0 ; clear_subset_proofs ; tauto.
+
+  apply H. simpl. omega.
+Qed.
+
+Program Fixpoint check_n'  (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p)
+  {measure (p - n) p} : nat :=
+  _.
-- 
cgit v1.2.3