Merge pull request #26 from coq-community/corrections

fix a few warnings

ch15_general_recursion/SRC/sqrt_nat_wf.v

@@ -68,11 +68,15 @@ refine (fun n sqrt_nat =>
        lia.
        ring.
        ring.
-Qed.
+Defined.
 
 Definition sqrt_nat' :
   forall n,  ({s : nat & {r : nat | n = s * s + r /\ n < (s + 1) * (s + 1)}}) :=
    well_founded_induction
     lt_wf
     (fun n => {s : nat & {r : nat | n = s * s + r /\ n < (s + 1) * (s + 1)}})
     sqrt_nat_F.
+
+
+
+

ch6_inductive_data/SRC/man_inj.v

@@ -4,23 +4,26 @@ Inductive htree (A:Set) : nat -> Set :=
   | hnode : forall n:nat, A -> htree A n -> htree A n -> htree A (S n).
 
 
-Definition first_of_htree :
-  forall (A:Set) (n:nat), htree A n -> htree A (S n) -> htree A n.
- intros A n v t.
- generalize v.
- change (htree A (pred (S n)) -> htree A (pred (S n))).
- case t.
- -  intros x v'; exact v'.
- -  intros p x t1 t2 v'; exact t1.
+Definition left_son {A:Set} {n:nat}: forall (t: htree A (S n)), htree A n :=
+  fun  t => match t in htree _ (S n) return htree A n with
+              hnode _ n a t1 t2 => t1
+            end.
+
+Definition left_son_interactive {A:Set} {n:nat}:
+  forall (t: htree A (S n)), htree A n.
+Proof.
+  intro t; change (htree A (pred (S n))).
+  destruct t as [a| n0 a t1 t2].
+  - exact (hleaf A a).
+  - exact t1.
 Defined.
- 
-Theorem injection_first_htree :
- forall (n:nat) (t1 t2 t3 t4:htree nat n),
-   hnode nat n 0 t1 t2 = hnode nat n 0 t3 t4 -> t1 = t3.
+
+Theorem injection_left_son :
+  forall (n:nat) (t1 t2 t3 t4:htree nat n),
+    hnode nat n 0 t1 t2 = hnode nat n 0 t3 t4 -> t1 = t3.
 Proof.
- intros n t1 t2 t3 t4 h.
- change
-  (first_of_htree nat n t1 (hnode nat n 0 t1 t2) =
-   first_of_htree nat n t1 (hnode nat n 0 t3 t4)).
- now  rewrite h.
-Qed.
+  intros * H; change (left_son (hnode nat n 0 t1 t2) =
+                      left_son (hnode nat n 0 t3 t4)).
+   now rewrite H.
+Qed. 
+

tutorial_type_classes/SRC/Lost_in_NY.v

@@ -73,9 +73,11 @@ Proof.  intros r r' H p; symmetry;apply H. Qed.
 Lemma route_equiv_trans : transitive _ route_equiv.
 Proof.  intros r r' r'' H H' p; rewrite H; apply H'. Qed.
 
-Instance route_equiv_Equiv : Equivalence  route_equiv.
+#[local] Instance route_equiv_Equiv : Equivalence  route_equiv.
 Proof.
-split;  [apply route_equiv_refl |  apply route_equiv_sym |  apply route_equiv_trans].
+  split;
+    [apply route_equiv_refl | apply route_equiv_sym |
+      apply route_equiv_trans].
 Qed.
 
 
@@ -90,7 +92,7 @@ Example Ex2 :  South::East::North::West::South::East::nil =r= South::East::nil.
 Proof. apply route_cons;apply Ex1. Qed.
 
 
-Instance cons_route_Proper (d:direction): 
+#[local] Instance cons_route_Proper (d:direction): 
     Proper (route_equiv ==> route_equiv) (cons d) .
 Proof.
  intros r r' H ; now apply route_cons.
@@ -107,7 +109,8 @@ Proof.
 Qed.
 
 
-Instance move_Proper  : Proper (route_equiv ==> @eq Point ==> @eq Point) move . 
+#[local] Instance move_Proper  :
+  Proper (route_equiv ==> @eq Point ==> @eq Point) move . 
 Proof.
  intros r r' Hr_r' p q Hpq; rewrite Hpq; apply Hr_r'.
 Qed.
@@ -128,8 +131,9 @@ Proof.
 Qed.
 
 
-Instance app_route_Proper : Proper (route_equiv==>route_equiv ==> route_equiv)
- (@app direction).
+#[local] Instance app_route_Proper :
+  Proper (route_equiv==>route_equiv ==> route_equiv)
+    (@app direction).
 Proof.
  intros r r' H r'' r''' H' P.
  repeat rewrite route_compose; rewrite H, H';reflexivity.
@@ -275,7 +279,7 @@ Qed.
 
 (** Monoid structure on routes *)
 
-Instance Route : EMonoid route_equiv (@app _)  nil .
+#[local] Instance Route : EMonoid route_equiv (@app _)  nil .
 Proof.
 split.
 - apply route_equiv_Equiv.
@@ -291,6 +295,6 @@ Proof.
  rewrite IHp; route_eq_tac.
 Qed.
 
-Instance AbelianRoute : Abelian_EMonoid Route. 
+#[local] Instance AbelianRoute : Abelian_EMonoid Route. 
   split;  apply app_comm.
 Qed.