blob: 81bdbc29f0a1241436ac9f5a65a946394bd32c8f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
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 :=
_.
|
