diff --git a/examples/Vector_tuple.v b/examples/Vector_tuple.v index 3b18a25..2fd852a 100644 --- a/examples/Vector_tuple.v +++ b/examples/Vector_tuple.v @@ -209,12 +209,8 @@ Defined. Module AppendConst. -Trocq Use Param2a0_nat. -Trocq Use Param_add. -Trocq Use Param02b_tuple_vector. -Trocq Use Param_append. -Trocq Use Param_const. -Trocq Use Param01_paths. +Trocq Use Param2a0_nat Param_add Param02b_tuple_vector. +Trocq Use Param_append Param_const Param01_paths. Lemma append_const : forall {A : Type} (a : A) (n1 n2 : nat), append (const a n1) (const a n2) = const a (n1 + n2). @@ -244,12 +240,7 @@ Definition Rp2a2b : Param2a2b.Rel Zp int := Rp42b. Lemma head_const {n : nat} : forall (i : int), Vector.hd (Vector.const i (S n)) = i. Proof. destruct n; simpl; reflexivity. Qed. -Trocq Use Param2a0_nat. -Trocq Use SR. -Trocq Use Rp2a2b. -Trocq Use Param_head. -Trocq Use Param_const. -Trocq Use Param01_paths. +Trocq Use Param2a0_nat SR Rp2a2b Param_head Param_const Param01_paths. Lemma head_const' : forall {n : nat} (z : Zp), head (const z (S n)) = z. Proof. trocq. exact @head_const. Qed. @@ -277,14 +268,9 @@ Proof. + exact vv'R. Defined. -Trocq Use SR. -Trocq Use Param_cons. -Trocq Use Param_add. -Trocq Use Param_append. -Trocq Use Param01_paths. -Trocq Use Param2a0_tuple_vector. -Trocq Use Param02b_tuple_vector. -Trocq Use Param2a0_nat. +Trocq Use SR Param_cons Param_add Param_append Param01_paths. +Trocq Use Param2a0_tuple_vector Param02b_tuple_vector Param2a0_nat. + Lemma append_comm_cons : forall {A : Type} {n1 n2 : nat} (v1 : tuple A n1) (v2 : tuple A n2) (a : A), @paths (tuple A (S (n1 + n2))) (cons a (append v1 v2)) (append (cons a v1) v2). @@ -449,13 +435,8 @@ Axiom setBitThenGetSame : (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b. -Trocq Use Param2a0_nat. -Trocq Use Param44_Bool. -Trocq Use Param2a0_bnat_bv. -Trocq Use getBitR. -Trocq Use setBitR. -Trocq Use Param01_paths. -Trocq Use Param10_lt. +Trocq Use Param2a0_nat Param44_Bool Param2a0_bnat_bv getBitR setBitR. +Trocq Use Param01_paths Param10_lt. Lemma setBitThenGetSame' : forall {k : nat} (bn : bounded_nat k) (i : nat) (b : Bool), diff --git a/examples/artifact_paper_example.v b/examples/artifact_paper_example.v index cdc9811..d532b45 100644 --- a/examples/artifact_paper_example.v +++ b/examples/artifact_paper_example.v @@ -30,7 +30,7 @@ Trocq Use RN. (* registering related types *) types: *) Definition RN0 : RN 0%N 0%nat. Proof. done. Defined. Definition RNS m n : RN m n -> RN (N.succ m) (S n). Proof. by case. Defined. -Trocq Use RN0. Trocq Use RNS. (* registering related constants *) +Trocq Use RN0 RNS. (* registering related constants *) (** We can now make use of the tactic to prove an induction principle on `N` *) Lemma N_Srec : forall (P : N -> Type), P 0%N -> diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index 6b74cf7..9db02f1 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -18,8 +18,10 @@ Set Universe Polymorphism. Declare Scope int_scope. Delimit Scope int_scope with int. +Local Open Scope int_scope. Declare Scope Zmodp_scope. Delimit Scope Zmodp_scope with Zmodp. +Local Open Scope Zmodp_scope. Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ (f : X -> Y -> Z) (g : X' -> Y' -> Z') := @@ -39,10 +41,16 @@ Axiom (modp : int -> Zmodp) (reprp : Zmodp -> int) Definition eqmodp (x y : int) := modp x = modp y. +(* for now translations need the support of a global reference: *) +Definition eq_Zmodp (x y : Zmodp) := (x = y). +Arguments eq_Zmodp /. + (* Axiom (eqp_refl : Reflexive eqmodp). *) (* Axiom (eqp_sym : Symmetric eqmodp). *) (* Axiom (eqp_trans : Transitive eqmodp). *) +Notation "0" := zero : int_scope. +Notation "0" := zerop : Zmodp_scope. Notation "x == y" := (eqmodp x%int y%int) (format "x == y", at level 70) : int_scope. Notation "x + y" := (add x%int y%int) : int_scope. @@ -54,31 +62,21 @@ Module IntToZmodp. Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK). -Axiom Rzero' : Rp zero zerop. -Variable Radd' : binop_param Rp Rp Rp add addp. -Variable Rmul' : binop_param Rp Rp Rp mul mulp. - -Trocq Use Rmul'. -Trocq Use Rzero'. -Trocq Use Param10_paths. -Trocq Use Rp. - -Definition eq_Zmodp (x y : Zmodp) := (x = y). -(* Bug if we inline the previous def in the following axiom *) -Axiom Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x -> +Axiom Rzero : Rp zero zerop. +Variable Radd : binop_param Rp Rp Rp add addp. +Variable Rmul : binop_param Rp Rp Rp mul mulp. +Variable Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x -> forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmodp x y). -Trocq Use Reqmodp01. -Arguments eq_Zmodp /. -Hypothesis RedZmodpEq0 : - (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = (p * p * p)%Zmodp -> - m = zerop). +Trocq Use Rp Rmul Rzero Param10_paths Reqmodp01. -Lemma IntRedModZp : forall (m n p : int), - (m = n * n)%int -> m = (p * p * p)%int -> eqmodp m zero. +Lemma IntRedModZp : + (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = 0) -> + forall (m n p : int), (m = n * n)%int -> (m == 0)%int. Proof. +move=> Hyp. trocq; simpl. -exact @RedZmodpEq0. +exact: Hyp. Qed. (* Print Assumptions IntRedModZp. (* No Univalence *) *) @@ -93,11 +91,7 @@ Axiom Rzero : Rp zerop zero. Variable Radd : binop_param Rp Rp Rp addp add. Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. -Trocq Use Rp. -Trocq Use Param01_paths. -Trocq Use Param10_paths. -Trocq Use Radd. -Trocq Use Rzero. +Trocq Use Rp Param01_paths Param10_paths Radd Rzero. Goal (forall x y, x + y = y + x)%Zmodp. Proof. diff --git a/examples/nat_ind.v b/examples/nat_ind.v index 86d6838..ace8f58 100644 --- a/examples/nat_ind.v +++ b/examples/nat_ind.v @@ -32,9 +32,7 @@ Definition RI : Param2a3.Rel I nat := Definition RI0 : RI I0 O. Proof. exact of_nat0. Qed. Definition RIS m n : RI m n -> RI (IS m) (S n). Proof. exact: of_natS. Qed. -Trocq Use RI. -Trocq Use RI0. -Trocq Use RIS. +Trocq Use RI RI0 RIS. Lemma I_Srec : forall (P : I -> Type), P I0 -> (forall n, P n -> P (IS n)) -> forall n, P n. diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index 0cedacd..84bb71c 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -30,9 +30,7 @@ Definition RN : Param2a3.Rel N nat := Definition RN0 : RN 0%N 0%nat. Proof. done. Qed. Definition RNS m n : RN m n -> RN m.+1%N n.+1%nat. Proof. by case. Qed. -Trocq Use RN. -Trocq Use RN0. -Trocq Use RNS. +Trocq Use RN RN0 RNS. Lemma N_Srec : forall (P : N -> Type), P N0 -> (forall n, P n -> P n.+1%N) -> forall n, P n. diff --git a/examples/summable.v b/examples/summable.v index 1f5b52f..1891128 100644 --- a/examples/summable.v +++ b/examples/summable.v @@ -203,12 +203,8 @@ move=> u _ <-; rewrite extend_truncate//. by apply isSummableP. Qed. -Trocq Use Param01_paths. -Trocq Use Param02b_nnR. -Trocq Use Param2a0_rseq. -Trocq Use R_sum_xnnR. -Trocq Use R_add_xnnR. -Trocq Use seq_nnR_add. +Trocq Use Param01_paths Param02b_nnR Param2a0_rseq. +Trocq Use R_sum_xnnR R_add_xnnR seq_nnR_add. (* we get a proof over non negative reals for free, from the analogous proof over the extended ones *) diff --git a/examples/trocq_gen_rewrite.v b/examples/trocq_gen_rewrite.v index 75d79fb..50e0800 100644 --- a/examples/trocq_gen_rewrite.v +++ b/examples/trocq_gen_rewrite.v @@ -54,15 +54,13 @@ apply: (@Param01.BuildRel (m <= n)%int (m' <= n')%int (fun _ _ => Unit)). - by constructor => mn; apply (le_morph _ _ Rm _ _ Rn). Qed. -Trocq Use le01. -Trocq Use add_morph. +Trocq Use le01 add_morph. Variables i j : int. Variable ip : (j <= i)%int. Definition iid : (i <= i)%int := le_refl i. -Trocq Use ip. -Trocq Use iid. +Trocq Use ip iid. Example ipi : (j + i + j <= i + i + i)%int. Proof. diff --git a/examples/trocq_setoid_rewrite.v b/examples/trocq_setoid_rewrite.v index 835eeaf..677653e 100644 --- a/examples/trocq_setoid_rewrite.v +++ b/examples/trocq_setoid_rewrite.v @@ -55,16 +55,14 @@ apply: (@Param01.BuildRel (m == n)%int (m' == n')%int (fun _ _ => Unit)). - by constructor => mn; apply (eqmodp_morph _ _ Rm _ _ Rn). Qed. -Trocq Use eqmodp01. -Trocq Use add_morph. +Trocq Use eqmodp01 add_morph. Variables i : int. Let j := (i + p)%int. Variable ip : (j == i)%int. Definition iid : (i == i)%int := eqp_refl i. -Trocq Use ip. -Trocq Use iid. +Trocq Use ip iid. Example ipi : (j + i == i + i)%int. Proof. diff --git a/theories/Vernac.v b/theories/Vernac.v index 6579977..f1a7544 100644 --- a/theories/Vernac.v +++ b/theories/Vernac.v @@ -111,6 +111,10 @@ Elpi Accumulate lp:{{ % (clause _ (before "default-gref") % (trocq.db.gref GR (pc map4 map2b) [] {{:gref int}} {{:gref Rp42b}})), + % serveral use in one go! + main [str "Use", X, Y | Rest] :- !, std.do![ + main [str "Use", X], main [str "Use", Y | Rest]]. + main [str "Usage"] :- !, coq.say {usage-msg}. main _ :- coq.error {std.string.concat "\n" ["command syntax error", {usage-msg}]}.