diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto3/theories')
| -rw-r--r-- | doc/plugin_tutorial/tuto3/theories/Data.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v index 0b07fee4f2..f7395d686b 100644 --- a/doc/plugin_tutorial/tuto3/theories/Data.v +++ b/doc/plugin_tutorial/tuto3/theories/Data.v @@ -1,4 +1,4 @@ -Require Import ArithRing. + Inductive pack (A: Type) : Type := packer : A -> pack A. @@ -18,7 +18,11 @@ Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}. Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}. Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n). -Proof. intros H; ring [H]. Qed. +Proof. + intros []. + simpl. rewrite <-plus_n_O, <-plus_n_Sm. + reflexivity. +Qed. Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) := {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}. @@ -51,7 +55,8 @@ Canonical Structure can_ev0 : S_ev 0 := Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). Proof. intros s; exists (S (S (double_of _ s))). -destruct s as [a P]. simpl. ring [P]. +destruct s as [a P]. +exact (even_rec _ _ P). Defined. Canonical Structure can_ev_rec. |