Merge pull request #17 from coq-community/add-proof-using

add `Proof using` annotations, either directly or through `Set Default Proof Using`.

theories/dfa.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Printing Implicit Defensive.
 Unset Strict Implicit.
@@ -155,6 +157,7 @@ Qed.
 Section CutOff.
   Variables (aT rT : finType) (f : seq aT -> rT).
   Hypothesis RC_f : forall x y a, f x = f y -> f (x++[::a]) = f (y++[::a]).
+  Local Set Default Proof Using "RC_f".
 
   Lemma RC_seq x y z : f x = f y -> f (x++z) = f (y++z).
   Proof.
@@ -279,7 +282,7 @@ Section Preimage.
      dfa_trans x a := delta x (h [:: a]) |}.
 
   Lemma dfa_preimP A : dfa_lang (dfa_preim A) =i preim h (dfa_lang A).
-  Proof. 
+  Proof using h_hom.
     move => w. rewrite !inE /dfa_accept /dfa_preim /=. 
     elim: w (dfa_s A) => [|a w IHw] x /= ; first by rewrite h0.
     by rewrite -[a :: w]cat1s h_hom !delta_cat -IHw.
@@ -316,7 +319,7 @@ Section RightQuotient.
        dfa_fin := [set q | dec_L2 q] |}.
 
   Lemma dfa_quotP x : reflect (quotR x) (x \in dfa_lang dfa_quot).
-  Proof.
+  Proof using acc_L1.
     apply: (iffP idP).
     - rewrite inE /dfa_accept inE. case/dec_eq => y inL2.
       rewrite -delta_cat => H. exists y => //. by rewrite -acc_L1.
@@ -363,7 +366,7 @@ Section LeftQuotient.
   Proof. rewrite inE /delta_s. elim: x (dfa_s A)=> //= a x IH q. by rewrite accE IH. Qed.
 
   Lemma regular_quotL_aux : regular quotL.
-  Proof.
+  Proof using acc_L2 dec_L1.
     pose S := [seq q | q <- enum A & dec_L1 q].
     pose L (q:A) := mem (dfa_lang (A_start q)).
     pose R x := exists2 a, a \in S & L a x.
@@ -433,21 +436,17 @@ Section NonRegular.
   Qed.
 
   Hypothesis (a b : char) (Hab : a != b).
+  Local Set Default Proof Using "Hab".
 
   Definition Lab w := exists n, w = nseq n a ++ nseq n b.
 
-  Lemma count_nseq (T : eqType) (c d : T) n :
-    count (pred1 c) (nseq n d) = (c == d) * n.
-  Proof.
-    elim: n => [|n] /=; first by rewrite muln0.
-    rewrite [d == c]eq_sym. by case e: (c == d) => /= ->.
-  Qed.
-
   Lemma countL n1 n2 : count (pred1 a) (nseq n1 a ++ nseq n2 b) = n1.
-  Proof. by rewrite count_cat !count_nseq (negbTE Hab) eqxx //= mul1n mul0n addn0. Qed.
+  Proof. 
+    by rewrite count_cat !count_nseq /= eqxx eq_sym (negbTE Hab) mul1n mul0n addn0. 
+  Qed.
 
   Lemma countR n1 n2 : count (pred1 b) (nseq n1 a ++ nseq n2 b) = n2.
-  Proof. by rewrite count_cat !count_nseq eq_sym (negbTE Hab) eqxx //= mul1n mul0n. Qed.
+  Proof. by rewrite count_cat !count_nseq /= (negbTE Hab) eqxx //= mul1n mul0n. Qed.
 
   Lemma Lab_eq n1 n2 : Lab (nseq n1 a ++ nseq n2 b) -> n1 = n2.
   Proof.

theories/languages.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -34,11 +36,19 @@ Section Basics.
 End Basics. 
 
 Section HomDef.
-  Variables (char char' : finType).
-  Variable (h : seq char -> seq char').
+  Variables (char char' : finType) (h : seq char -> seq char').
+
+  Definition image (L : word char -> Prop) v := exists w, L w /\ h w = v.
+
+  Lemma image_ext L1 L2  w :
+    (forall v, L1 v <-> L2 v) -> (image L1 w <-> image L2 w).
+  Proof. by move => H; split; move => [v] [] /H; exists v. Qed.
+
+  Definition preimage (L : word char' -> Prop) v :=  L (h v).
 
   Definition homomorphism := forall w1 w2, h (w1 ++ w2) = h w1 ++ h w2.
   Hypothesis h_hom : homomorphism.
+  Local Set Default Proof Using "h_hom".  
 
   Lemma h0 : h [::] = [::].
   Proof.
@@ -55,15 +65,6 @@ Section HomDef.
     by rewrite h_hom IHvv.
   Qed.
 
-  Definition image (L : word char -> Prop) v := exists w, L w /\ h w = v.
-
-  Lemma image_ext L1 L2  w :
-    (forall v, L1 v <-> L2 v) -> (image L1 w <-> image L2 w).
-  Proof. by move => H; split; move => [v] [] /H; exists v. Qed.
-
-  Definition preimage (L : word char' -> Prop) v :=  L (h v).
-
-
 End HomDef.
 
 (** ** Closure Properties for Decidable Languages *)

theories/minimization.v

@@ -4,6 +4,8 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype path fingraph finfun finset generic_quotient.
 From RegLang Require Import misc languages dfa.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Printing Implicit Defensive.
 Unset Strict Implicit.
@@ -43,19 +45,19 @@ Section Isomopism.
   Definition iso_inv := delta_s A \o cr B_conn.
 
   Lemma delta_iso w x : delta (iso x) w \in dfa_fin B = (delta x w \in dfa_fin A).
-  Proof. by rewrite -{2}[x](crK (Sf := A_conn)) -!delta_cat !delta_lang L_AB. Qed.
+  Proof using L_AB. by rewrite -{2}[x](crK (Sf := A_conn)) -!delta_cat !delta_lang L_AB. Qed.
 
   Lemma delta_iso_inv w x : delta (iso_inv x) w \in dfa_fin A = (delta x w \in dfa_fin B).
-  Proof. by rewrite -{2}[x](crK (Sf := B_conn)) -!delta_cat !delta_lang L_AB. Qed.
+  Proof using L_AB. by rewrite -{2}[x](crK (Sf := B_conn)) -!delta_cat !delta_lang L_AB. Qed.
 
   Lemma can_iso : cancel iso_inv iso.
-  Proof. move => x. apply/B_coll => w. by rewrite delta_iso delta_iso_inv. Qed.
+  Proof using B_coll L_AB. move => x. apply/B_coll => w. by rewrite delta_iso delta_iso_inv. Qed.
 
   Lemma can_iso_inv : cancel iso iso_inv.
-  Proof. move => x. apply/A_coll => w. by rewrite delta_iso_inv delta_iso. Qed.
+  Proof using A_coll L_AB. move => x. apply/A_coll => w. by rewrite delta_iso_inv delta_iso. Qed.
 
   Lemma coll_iso : dfa_iso A B.
-  Proof.
+  Proof using A_coll B_coll A_conn B_conn L_AB.
     exists iso. split.
     - exact: Bijective can_iso_inv can_iso.
     - move => x a. apply/B_coll => w. rewrite -[_ (iso x) a]/(delta (iso x) [::a]).

theories/misc.v

@@ -3,6 +3,8 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -212,7 +214,8 @@ Section Functional.
   Hypothesis f_inv: forall x z, e' (f x) z -> exists y, z = f y. 
 
   Lemma connect_transfer x y : connect e x y = connect e' (f x) (f y).
-  Proof. apply/idP/idP.
+  Proof using f_eq f_inj f_inv.
+    apply/idP/idP.
     - case/connectP => s.
       elim: s x => //= [x _ -> |z s IH x]; first exact: connect0.
       case/andP => xz pth Hy. rewrite f_eq in xz.
@@ -221,7 +224,7 @@ Section Functional.
       elim: s x => //= [x _ /f_inj -> |z s IH x]; first exact: connect0.
       case/andP => xz pth Hy. case: (f_inv xz) => z' ?; subst. 
       rewrite -f_eq in xz. apply: connect_trans (connect1 xz) _. exact: IH.
-  Qed.  
+  Qed.
 End Functional.
 
 Lemma functional_sub (T : finType) (e1 e2 : rel T) : 
@@ -257,7 +260,3 @@ Proof. by rewrite (eqP (xchooseP (Sf x))). Qed.
 
 Lemma dec_eq (P : Prop) (decP : decidable P) : decP <-> P.
 Proof. by case: decP. Qed.
-
-
-
-

theories/myhill_nerode.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages dfa minimization regexp.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -182,7 +184,7 @@ Section mDFAtoMG.
   Variable MA : minimal A.
 
   Lemma minimal_nerode : nerode (dfa_lang A) (delta_s A).
-  Proof.
+  Proof using MA.
     move => u v. apply: iff_trans (iff_sym (minimal_collapsed MA _ _)) _.
     by split => H w; move: (H w); rewrite -!delta_cat !delta_lang.
   Qed.

theories/nfa.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages dfa.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Printing Implicit Defensive.
 Unset Strict Implicit.

theories/regexp.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import setoid_leq misc languages dfa nfa.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -408,7 +410,7 @@ Section Image.
     end.
 
   Lemma re_imageP e v : reflect (image h (re_lang e) v) (v \in re_image e).
-  Proof.
+  Proof using h_hom.
     elim: e v => [||a|e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2] v /=.
     - rewrite inE; constructor. move => [u]. by case.
     - rewrite inE; apply: (iffP eqP) => [-> |[w] [] /eqP -> <-]; last exact: h0.

theories/shepherdson.v

@@ -4,6 +4,8 @@ From Coq Require Import Omega.
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc setoid_leq languages dfa myhill_nerode two_way.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -12,7 +14,7 @@ Unset Printing Implicit Defensive.
 
 (** Preliminaries *)
 
-Lemma contraN (b : bool) (P : Prop) : b -> ~~ b -> P. by case b. Qed. 
+Lemma contraN (b : bool) (P : Prop) : b -> ~~ b -> P. Proof. by case b. Qed.
 
 Lemma inord_inj n m : n <= m -> injective (@inord m \o @nat_of_ord n.+1).
 Proof.

theories/two_way.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages dfa regexp myhill_nerode.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -192,7 +194,6 @@ Section DFAtoDFA2.
   Lemma nfa2_of_aux2 (q f:A) (i : pos w) : i != ord0 ->
     f \in nfa2_f nfa2_of_dfa -> connect (step nfa2_of_dfa w) (q,i) (f,ord_max) -> 
     ((drop i.-1 w) \in dfa_accept q).
-  Proof.
   Proof.
     move => H fin_f. case/connectP => p. elim: p i H q => //= [|[q' j] p IHp i Hi q].
     - move => i Hi q _ [<- <-]. rewrite drop_size -topredE /= accept_nil. by rewrite inE in fin_f.

theories/vardi.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages nfa two_way.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

theories/wmso.v

@@ -3,6 +3,8 @@
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages dfa nfa regexp.
 
+Set Default Proof Using "Type".
+
 Set Implicit Arguments.
 Unset Printing Implicit Defensive.
 Unset Strict Implicit.