Skip to content
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

Fix for coq PR #13969 #32

Merged
merged 1 commit into from
Jan 4, 2022
Merged

Fix for coq PR #13969 #32

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
2 changes: 2 additions & 0 deletions lattice.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,8 @@ Proof.
intros x y z. rewrite 3weq_spec. intuition; etransitivity; eassumption.
Qed.

#[export] Instance weq_rel {ops} : RewriteRelation (@weq ops) := {}.

#[export] Instance weq_leq `{laws}: subrelation weq leq.
Proof. intros x y E. apply weq_spec in E as [? ?]. assumption. Qed.

Expand Down
2 changes: 1 addition & 1 deletion matrix.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -352,7 +352,7 @@ Lemma mx_dot_rowcol n m1 m2 p (M1: mx n m1) (M2: mx n m2) (N1: mx m1 p) (N2: mx
row_mx M1 M2 ⋅ col_mx N1 N2 ≡ M1⋅N1 + M2⋅N2.
Proof.
intros i j. setoid_rewrite sup_cut. unfold row_mx, col_mx.
setoid_rewrite split_lshift. setoid_rewrite split_rshift. reflexivity. (* LONG *)
setoid_rewrite split_lshift. setoid_rewrite split_rshift. reflexivity.
Qed.

Lemma mx_dot_blk n1 n2 m1 m2 p1 p2
Expand Down