Stream: math-comp users

Topic: coqeal example


view this post on Zulip Julin Shaji (Oct 18 2023 at 04:45):

I was trying one of the examples mentioned at the end of https://github.com/coq-community/coqeal/blob/1.1.3/refinements/seqmx.v#L1379C1-L1382C7

This one (with coqeal 1.1.3 and mathcomp-1):

From CoqEAL Require Import hrel param refinements trivial_seq.
From CoqEAL.refinements Require Import seqmx.


Goal ((0 : 'M[int]_(2,2)) == 0).
  by coqeal.
Abort.

But that gave error (no applicable tactic).
The same coqeal tactic without the by leads to a loong term.

How can I make this work?

view this post on Zulip Julin Shaji (Oct 18 2023 at 05:28):

This went ahead though:

Goal ((0 : 'M[int]_(2,2)) == 0).
  rewrite /const_mx //.
Qed.

view this post on Zulip Pierre Roux (Oct 18 2023 at 14:33):

Apparently there were a few missing require imports, the following works (the set of require import may not be minimal though):

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
From mathcomp Require Import ssralg matrix ssrint.
From CoqEAL Require Import hrel param refinements trivial_seq.
From CoqEAL Require Import binnat binint seqpoly binord seqmx.

Local Open Scope ring_scope.

Section testmx.

Goal ((0 : 'M[int]_(2,2)) == 0).
by coqeal.
Abort.

Last updated: Jul 15 2024 at 20:02 UTC