Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21611 #51

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Mar 5, 2026
Merged

Adapt to https://github.com/rocq-prover/rocq/pull/21611 #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions theories/core/open_confluence.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -947,7 +947,7 @@ Proof.
- by rewrite eqxx orbT eq_sym E3 eq_sym E2.
Qed.

Lemma critical_pair1 (u v a : tm) of is_test a : dom ((u∥v°)·a) ≡ 1 ∥ u·a·v.
Lemma critical_pair1 (u v a : tm) & is_test a : dom ((u∥v°)·a) ≡ 1 ∥ u·a·v.
Proof. by rewrite -dotA A10 cnvdot cnvtst partst. Qed.

Lemma critical_pair2 (u v : tm) : (1∥u)·(1∥v) ≡ 1∥(u∥v).
Expand All @@ -956,7 +956,7 @@ Proof.
by rewrite parA [_∥1]parC !parA par11.
Qed.

Lemma critical_pair3 (u u' a b : tm) of is_test a & is_test b :
Lemma critical_pair3 (u u' a b : tm) & is_test a & is_test b :
dom (u'·(dom (u·a)·b)) ≡ dom (u'·b·u·a).
by rewrite dotC /= dotA -A13 !dotA.
Qed.
Expand Down
4 changes: 2 additions & 2 deletions theories/core/ptt.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,14 @@
for [dom], (i.e., [A13] and [A14]) can be omitted, as they are
derivable *)

HB.mixin Record Ptt_of_Pttdom A of Pttdom A :=
HB.mixin Record Ptt_of_Pttdom A & Pttdom A :=
{ A11: forall x: A, x · top ≡ dom x · top;
A12: forall x y: A, (x∥1) · y ≡ (x∥1)·top ∥ y;
domE: forall x: A, dom x ≡ 1 ∥ x·top }.
HB.structure Definition Ptt := { A of Ptt_of_Pttdom A & }.
Notation ptt := Ptt.type.

HB.factory Record Ptt_of_Ops A of Ops_of_Type A & Setoid_of_Type A :=
HB.factory Record Ptt_of_Ops A & Ops_of_Type A & Setoid_of_Type A :=
{ dot_eqv: Proper (eqv ==> eqv ==> eqv) (dot : A -> A -> A);
par_eqv: Proper (eqv ==> eqv ==> eqv) (par : A -> A -> A);
cnv_eqv: Proper (eqv ==> eqv) (cnv : A -> A);
Expand Down Expand Up @@ -145,7 +145,7 @@
HB.instance Definition tm_ops := Ops_of_Type.Build term tm_dot tm_par tm_cnv tm_dom tm_one tm_top.

Let tm_eqv_eqv (u v: term) (X: ptt) (f: A -> X) : u ≡ v -> eval f u ≡ eval f v.
Proof. exact. Qed.

Check warning on line 148 in theories/core/ptt.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

tm_eqv_eqv is declared opaque (Qed) but this is not fully respected

(* quotiented terms indeed form a 2p algebra *)
Definition tm_ptt : Ptt_of_Ops.axioms_ term tm_ops tm_setoid.
Expand Down
36 changes: 18 additions & 18 deletions theories/core/pttdom.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ Notation "1" := (one): pttdom_ops.

(* 2pdom axioms *)

HB.mixin Record Pttdom_of_Ops A of Ops_of_Type A & Setoid_of_Type A :=
HB.mixin Record Pttdom_of_Ops A & Ops_of_Type A & Setoid_of_Type A :=
{ dot_eqv: Proper (eqv ==> eqv ==> eqv) (dot : A -> A -> A);
par_eqv: Proper (eqv ==> eqv ==> eqv) (par : A -> A -> A);
cnv_eqv: Proper (eqv ==> eqv) (cnv : A -> A);
Expand Down Expand Up @@ -104,10 +104,10 @@ Section derived.
- by rewrite -E -{1}cnv1 -A10 dotx1 parC.
Qed.

Lemma domtst a of is_test a : dom a ≡ a.
Lemma domtst a & is_test a : dom a ≡ a.
Proof. exact: testE. Qed.

Lemma tstpar1 a of is_test a : a ∥ 1 ≡ a.
Lemma tstpar1 a & is_test a : a ∥ 1 ≡ a.
Proof. by apply/is_test_alt; rewrite domtst. Qed.

Lemma one_test: is_test (1:X).
Expand All @@ -118,38 +118,38 @@ Section derived.
Proof. constructor. by rewrite -{1}[dom x]dot1x -A13 dot1x. Qed.
Global Existing Instance dom_test.

Lemma par_test a u of is_test a : is_test (a∥u).
Lemma par_test a u & is_test a : is_test (a∥u).
Proof.
constructor; apply/is_test_alt.
by rewrite -parA (parC u) parA tstpar1.
Qed.
Global Existing Instance par_test.

Lemma cnvtst a of is_test a : a° ≡ a.
Lemma cnvtst a & is_test a : a° ≡ a.
Proof.
rewrite -[a]tstpar1 cnvpar cnv1 -(dot1x (a°)) parC A10 cnvI parC.
apply: domtst.
Qed.

Lemma cnv_test a of is_test a : is_test (a°).
Lemma cnv_test a & is_test a : is_test (a°).
Proof. constructor. by rewrite is_test_alt cnvtst tstpar1. Qed.
Global Existing Instance cnv_test.

Lemma tstpar a x y of is_test a : a·(x∥y) ≡ a·x ∥ y.
Lemma tstpar a x y & is_test a : a·(x∥y) ≡ a·x ∥ y.
Proof. rewrite -[a]domtst. apply A14. Qed.

Lemma tstpar_r a x y of is_test a : a·(x∥y) ≡ x ∥ a·y.
Lemma tstpar_r a x y & is_test a : a·(x∥y) ≡ x ∥ a·y.
Proof. by rewrite parC tstpar parC. Qed.

Lemma pardot a b of is_test a & is_test b : a ∥ b ≡ a·b.
Lemma pardot a b & is_test a & is_test b : a ∥ b ≡ a·b.
Proof.
by rewrite -{2}(@tstpar1 b) (parC _ 1) tstpar dotx1.
Qed.

Lemma dotC a b of is_test a & is_test b : a·b ≡ b·a.
Lemma dotC a b & is_test a & is_test b : a·b ≡ b·a.
Proof. by rewrite -pardot parC pardot. Qed.

Lemma dot_test a b of is_test a & is_test b : is_test (a·b).
Lemma dot_test a b & is_test a & is_test b : is_test (a·b).
Proof. constructor. rewrite -pardot. apply: domtst. Qed.
Global Existing Instance dot_test.

Expand All @@ -169,9 +169,9 @@ Section derived.
HB.instance Definition pttdom_test_setoid :=
Setoid_of_Type.Build test eqv_test_equiv.

Lemma infer_testE a of is_test a : elem_of [a] ≡ a.
Lemma infer_testE a & is_test a : elem_of [a] ≡ a.
Proof. by []. Qed.
Lemma eqv_testE a b of is_test a & is_test b : [a] ≡ [b] <-> a ≡ b.
Lemma eqv_testE a b & is_test a & is_test b : [a] ≡ [b] <-> a ≡ b.
Proof. by []. Qed.

Section M.
Expand Down Expand Up @@ -220,28 +220,28 @@ Section derived.

(** ** other derivable laws used in the completeness proof *)

Lemma partst u v a of is_test a : (u ∥ v)·a ≡ u ∥ v·a.
Lemma partst u v a & is_test a : (u ∥ v)·a ≡ u ∥ v·a.
Proof.
apply cnv_inj. rewrite cnvdot 2!cnvpar cnvdot.
by rewrite parC tstpar parC.
Qed.

Lemma par_tst_cnv a u of is_test a : a ∥ u° ≡ a ∥ u.
Lemma par_tst_cnv a u & is_test a : a ∥ u° ≡ a ∥ u.
Proof. by rewrite -[a∥u°]cnvtst cnvpar cnvtst cnvI. Qed.

Lemma eqvb_par1 a u v (b : bool) of is_test a : u ≡[b] v -> a ∥ u ≡ a ∥ v.
Lemma eqvb_par1 a u v (b : bool) & is_test a : u ≡[b] v -> a ∥ u ≡ a ∥ v.
Proof. case: b => [->|-> //]. exact: par_tst_cnv. Qed.

(* used twice in reduce in reduction.v *)
Lemma reduce_shuffle v a c d of is_test a & is_test c & is_test d :
Lemma reduce_shuffle v a c d & is_test a & is_test c & is_test d :
c·(d·a)·(1∥v) ≡ a ∥ c·v·d.
Proof.
rewrite -!dotA -tstpar_r; apply: dot_eqv => //.
by rewrite -partst tstpar dotx1 dotC.
Qed.

(* lemma for nt_correct *)
Lemma par_nontest u v a b c d of is_test a & is_test b & is_test c & is_test d :
Lemma par_nontest u v a b c d & is_test a & is_test b & is_test c & is_test d :
a·u·b∥c·v·d ≡ (a·c)·(u∥v)·(b·d).
Proof. by rewrite -partst -[a·u·b]dotA -tstpar parC -tstpar -partst !dotA parC. Qed.

Expand Down
4 changes: 2 additions & 2 deletions theories/core/structures.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From HB Require Import structures.
From Coq Require Import RelationClasses Morphisms Relation_Definitions.

Check warning on line 2 in theories/core/structures.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

"From Coq" has been replaced by "From Stdlib".
From mathcomp Require Import all_ssreflect.
From GraphTheory Require Import edone preliminaries setoid_bigop bij.

Expand Down Expand Up @@ -67,7 +67,7 @@
Global Existing Instance lv_monoid.
*)

HB.mixin Record ComMonoid_of_Setoid A of Setoid_of_Type A :=
HB.mixin Record ComMonoid_of_Setoid A & Setoid_of_Type A :=
{ cm_id : A;
cm_op : A -> A -> A;
cm_laws : comMonoidLaws cm_id cm_op }.
Expand All @@ -86,7 +86,7 @@
- eqv' x y = eqv x y° (when we have an involution _°)
- eqv' _ _ = False (otherwise) *)

HB.mixin Record Elabel_of_Setoid A of Setoid_of_Type A :=
HB.mixin Record Elabel_of_Setoid A & Setoid_of_Type A :=
{ eqv': Relation_Definitions.relation A;
Eqv'_sym: Symmetric eqv';
eqv01: forall x y z : A, eqv x y -> eqv' y z -> eqv' x z;
Expand Down Expand Up @@ -164,9 +164,9 @@
Section E.
Variable (A : Type).
Let rel := (fun _ _ : A => False).
Let rel_sym : Symmetric rel. by []. Qed.

Check warning on line 167 in theories/core/structures.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

rel_sym is declared opaque (Qed) but this is not fully respected
Let rel01 (x y z : A) : x = y -> rel y z -> rel x z. by []. Qed.

Check warning on line 168 in theories/core/structures.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

rel01 is declared opaque (Qed) but this is not fully respected
Let rel11 (x y z : A) : rel x y -> rel y z -> x = z. by []. Qed.

Check warning on line 169 in theories/core/structures.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

rel11 is declared opaque (Qed) but this is not fully respected

HB.instance Definition flat_elabel_mixin :=
@Elabel_of_Setoid.Build (flat A) rel rel_sym rel01 rel11.
Expand Down
Loading