Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'

git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b

1 files changed, 68 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v
new file mode 100644
index 0000000000..0b07fee4f2
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/theories/Data.v
@@ -0,0 +1,68 @@
+Require Import ArithRing.
+
+Inductive pack (A: Type) : Type :=
+  packer : A -> pack A.
+
+Arguments packer {A}.
+
+Definition uncover (A : Type) (packed : pack A) : A :=
+  match packed with packer v => v end.
+
+Notation "!!!" := (pack _) (at level 0, only printing).
+
+(* The following data is used as material for automatic proofs
+  based on type classes. *)
+
+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.
+
+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)}.
+
+Definition tuto_div2 n (p : EvenNat n) := @half _ p.
+
+(* to be used in the following examples
+Compute (@half 8 _).
+
+Check (@half_prop 8 _).
+
+Check (@half_prop 7 _).
+
+and in command Tuto3_3 8. *)
+
+(* The following data is used as material for automatic proofs
+  based on canonical structures. *)
+
+Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}.
+
+Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
+  match r with Build_S_ev _ _ h => h end.
+
+Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n :=
+  Build_S_ev n d Pd.
+
+Canonical Structure can_ev0 : S_ev 0 :=
+  Build_S_ev 0 0 (@eq_refl _ 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].
+Defined.
+
+Canonical Structure can_ev_rec.
+
+Record cmp (n : nat) (k : nat) :=
+  C {h : S_ev k; _ : double_of k h = n}.
+
+(* To be used in, e.g.,
+
+Check (C _ _ _ eq_refl : cmp 6 _).
+
+Check (C _ _ _ eq_refl : cmp 7 _).
+
+*)