diff options
Diffstat (limited to 'doc/plugin_tutorial')
| -rw-r--r-- | doc/plugin_tutorial/Makefile | 21 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto3/theories/Data.v | 11 |
2 files changed, 29 insertions, 3 deletions
diff --git a/doc/plugin_tutorial/Makefile b/doc/plugin_tutorial/Makefile new file mode 100644 index 0000000000..7f1833fadd --- /dev/null +++ b/doc/plugin_tutorial/Makefile @@ -0,0 +1,21 @@ + +TUTOS:= \ + tuto0 \ + tuto1 \ + tuto2 \ + tuto3 + +all: $(TUTOS) + +.PHONY: $(TUTOS) all + +$(TUTOS): %: + +$(MAKE) -C $@ + +CLEANS:=$(addsuffix -clean, $(TUTOS)) +.PHONY: clean $(CLEANS) + +clean: $(CLEANS) + +%-clean: + +$(MAKE) -C $* clean 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. |