Having first steps. Tried using `eqType`

... How should I proceed with this definition?

```
Require Import mathcomp.ssreflect.eqtype.
Require Import List.
Set Implicit Arguments.
Definition test (A: eqType): forall (a: A) (L: list A), {In a L} + {~ In a L}.
Proof.
intros. induction L.
+ simpl. right. auto.
+ simpl. destruct IHL.
- left. auto.
- admit.
Admitted.
```

What should I read to get more experienced with math-comp... that's probably the next question.

Thanks in advance.

in MathComp, you should use `seq`

instead of `list`

, and use the `\in`

notation for list containment. MathComp also doesn't much use sigma types like `{...}+{...}`

(boolean-returning functions are used instead). I'd recommend starting out by looking at the MathComp book: https://github.com/math-comp/mcb

Furthermore I think many things don't work as intended if you don't import at least `ssreflect`

, `ssrfun`

, and `ssrbool`

. For playing around it's often convenient to `From mathcomp Require Import all_ssreflect`

.

Yay, I achieved something.

```
From mathcomp Require Import all_ssreflect.
Require Import Utf8.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition testP (A: eqType) (S: seq A): ∀ a, reflect (List.In a S) (a \in S).
Proof.
intros. induction S.
+ simpl. compute. apply ReflectF. auto.
+ rewrite in_cons orbC; simpl. inversion IHS.
- apply ReflectT. auto.
- simpl. pose proof (@eqP A a a0). inversion H1.
* apply ReflectT. auto.
* apply ReflectF. intuition.
Qed.
```

Postponing learning Ssreflect tactic language for now... I have some resistance to it, as it feels like terrible Perl or smth at the start, and it can't be learned in a flash anyway.

But I will learn it sooner or later, just to know and understand it. Probably will use it too, I hope.

The PnP book https://ilyasergey.net/pnp/pnp.pdf may be useful for learning quietly ssreflect ...

A question... is there something like `map`

and also `fold_right`

that works on `T^n`

?

use canonical big operators: https://www-sop.inria.fr/marelle/bigops/main.pdf

Thank you!

It's probably my fault/mistake somehow, but I tried it and got an error message `Found type "(A ^ n)%type" where "Finite.sort ?T" was expected.`

:(

```
From mathcomp Require Import all_ssreflect.
Require Import Utf8.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section test.
Variables A: Type.
Variable f: A -> A -> A.
Variable a0: A.
Variable n: nat.
Variable V: A^n.
Check (\big[f/a0]_(i:A^n) V).
End test.
```

`\big_(i : T) _`

requires `T`

to be a `finType`

and for `A^n`

to be a `finType`

you need `A : finType`

instead of `A : Type`

I would say

It didn't help, sadly. I changed `A: Type`

to `A: finType`

and got message `The term "V" has type "(A ^ n)%type" while it is expected to have type "Finite.sort A".`

Now the problem moved from `(i:A^n)`

to `V`

.

`Check (\big[f/a0]_(i: 'I_n) V i).`

would work here. Note that `A^n`

here is a notation for finite function`'I_n -> A`

, i.e. essentially an n-tuple of A's, so this a right fold of a form `f (V 0) (f (V 1) ... (f (V n-1) a0) .. )`

Thank you!

When I tried to make analogue of `Forall`

using bigop (like in `fold_right (λ x : A, and (P x)) True l`

), I had problems.

What's the correct way to do what I'm trying?

```
From mathcomp Require Import all_ssreflect.
Require Import Utf8.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Structure Language F R := {
function_arity: F → nat;
relation_arity: R → nat
}.
Inductive Term F R (V: eqType) (L: Language F R) :=
| variable: V -> Term V L
| function_term: ∀ (f: F), (Term V L)^(function_arity L f) → Term V L.
Fixpoint term_has_variable F R (V: eqType) (L: Language F R) (i: V) (t: Term V L) :=
match t with
| variable v => v == i
| function_term f v =>
(\big[(λ (x: Term _ L), or (term_has_variable i x))/False]_(i:'I_ _) V i) end.
```

Lessness said:

Yay, I achieved something.

`From mathcomp Require Import all_ssreflect. Require Import Utf8. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Definition testP (A: eqType) (S: seq A): ∀ a, reflect (List.In a S) (a \in S). Proof. intros. induction S. + simpl. compute. apply ReflectF. auto. + rewrite in_cons orbC; simpl. inversion IHS. - apply ReflectT. auto. - simpl. pose proof (@eqP A a a0). inversion H1. * apply ReflectT. auto. * apply ReflectF. intuition. Qed.`

Just for comparison purpose (and the fun of it), here is my take on a ssreflect version of this lemma, loosely following your proof outline and with no automation:

```
Definition testP (A: eqType) (S: seq A): ∀ a, reflect (List.In a S) (a \in S).
Proof.
elim: S => [//= a|a S IH a0]; first exact: ReflectF.
rewrite in_cons /=.
apply: Bool.iff_reflect;
split=> [[->|/IH ->]|/orP [/eqP ->|/IH]].
- by rewrite eq_refl orTb.
- by rewrite orbT.
- by left.
- by right.
Qed.
```

We could even

```
Definition testP (A: eqType) (S: seq A): ∀ a, reflect (List.In a S) (a \in S).
Proof.
elim: S ⇒ [a|a S IH x]; first exact: ReflectF.
rewrite in_cons /=; apply/orPP.
- rewrite eq_sym; exact: eqP.
- exact: IH.
Qed.
```

(but trying to establish links between MC and the stdlib looks strange (except if you really need to reuse something based on the stdlib))

What stdlib types are idiomatic to use in ssreflect?

the high level answer is (I think): "use whatever is in the stdlib for things that have not ended up in an idiomatic MathComp project yet"

in the Coq Ecosystem talk/paper by Appel, I think there was a scenario where he and his collaborators wrote a separate MathComp layer for some piece of a non-MathComp library they needed

but I think there are some sigma types and other similar things are used in MathComp, but sparingly

What's the counterpart of `\in`

then, if not `List.In`

?

Anyway, I just thought that it is the MathComp way of doing decidable statements and did it for training purposes.

Lessness said:

When I tried to make analogue of

`Forall`

using bigop (like in`fold_right (λ x : A, and (P x)) True l`

), I had problems.

What's the correct way to do what I'm trying?

...

I used indexed list type previously (with `fold_right`

defined for it), then everything was okay:

```
Inductive vector A: nat -> Type :=
| vnil: vector A 0
| vcons: forall n, A -> vector A n -> vector A (S n).
```

Should I return to it, maybe?

the closest to `\in`

for lists is arguably: https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html#in_dec

For lists with a fixed size there is the mathcomp `tuple`

, and for lists of bounded size you can find `bseq`

in the same file.

Ana de Almeida Borges said:

For lists with a fixed size there is the mathcomp

`tuple`

, and for lists of bounded size you can find`bseq`

in the same file.

When I try to define tree-like structure with `tuple`

, I get `Non strictly positive occurrence`

error message. This is the reason I have chosen `T^n`

.

```
Inductive tree A :=
| leaf: A -> tree A
| forest: forall n, n.-tuple (tree A) -> tree A.
```

I would say that the mathcomp conterpart to `Forall`

is `all`

(defined in `seq`

). It's not actually a counterpart because `Forall`

lives in `Prop`

and `all`

lives in `bool`

(just as what happens with `In`

and `\in`

), but that's going to keep happening. MathComp tries to define as many things in `bool`

as possible.

When I try to define tree-like structure with tuple, I get Non strictly positive occurrence error message

Right, I'd forgotten about that. Note, however, that `T^n`

is isomorphic to `n.-tuple T`

. It's useful exactly for defining things where you need strict positivity.

Regarding your `term_has_variable`

function, I guess you are looking for an `Exists`

counterpart, and that would be `has`

. Thus this is how I would write it:

```
Fixpoint term_has_variable F R (V: eqType) (L: Language F R) (i: V) (t: Term V L) :=
match t with
| variable v => v == i
| function_term f v => has (term_has_variable i) (fgraph v)
end.
```

Where `fgraph`

`v`

is the tuple presentation of `v`

. However, Coq doesn't accept this definition because it cannot guess the decreasing argument. Unless there is some different approach, the path would be to define some measure on terms and use it to prove that this function terminates.

Following the example from https://math-comp.github.io/htmldoc/mathcomp.ssreflect.finfun.html (`Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1.`

), I wrote `term_has_variable`

in the following way.

```
From mathcomp Require Import all_ssreflect.
Require Import Utf8.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Structure Language F R := {
function_arity: F → nat;
relation_arity: R → nat
}.
Inductive Term F R (V: eqType) (L: Language F R) :=
| variable: V -> Term V L
| function_term: ∀ (f: F), (Term V L)^(function_arity L f) → Term V L.
Fixpoint term_has_variable F R (V: eqType) (L: Language F R) (i: V) (t: Term V L) {struct t}: bool :=
match t with
| variable x => (i == x)
| function_term f t' => has (eqb true) (codom (term_has_variable i \o t'))
end.
```

I got such error message when trying to rewrite. (I can post the code if necessary.)

```
The 6th term has type "relation_arity L r = relation_arity L (relation_map0 r)" which should be coercible to
"relation_arity L r = relation_arity L (_pattern_value_ r)".
```

What does this error message mean? What's that `_pattern_value_`

?

I've never seen that. Feel free to post the code.

Okay, the code.

```
From mathcomp Require Import all_ssreflect.
Require Import Utf8.
Import EqNotations.
Set Implicit Arguments.
Definition vmap A B n (f: A → B) (v: A^n): B^n := finfun (f \o v).
Structure Language F R := {
function_arity: F → nat;
relation_arity: R → nat
}.
Definition Function A n := A^n → A.
Definition Relation A n := A^n → Prop.
Structure Structure {F R} (L: Language F R) := {
domain: Type;
function: ∀ (f: F), Function domain (function_arity L f);
relation: ∀ (r: R), Relation domain (relation_arity L r)
}.
Inductive Term F R (V: eqType) (L: Language F R) :=
| variable: V → Term V L
| function_term: ∀ (f: F), (Term V L)^(function_arity L f) → Term V L.
Inductive Formula F R (V: eqType) (L: Language F R) :=
| atomic_formula: ∀ (r: R), (Term V L)^(relation_arity L r) → Formula V L
| negation: Formula V L → Formula V L
| disjunction: Formula V L → Formula V L → Formula V L
| conjunction: Formula V L → Formula V L → Formula V L
| existence_quantor: V → Formula V L → Formula V L
| universal_quantor: V → Formula V L → Formula V L.
Fixpoint interpreted_term F R (V: eqType) (L: Language F R) (M: Structure L) (assignment: V → domain M) (T: Term V L): domain M :=
match T with
| variable x => assignment x
| function_term f v => function M f (finfun (interpreted_term M assignment \o v))
end.
Fixpoint satisfies F R (V: eqType) (L: Language F R) (M: Structure L) (A: Formula V L) (assignment: V → domain M): Prop :=
match A with
| atomic_formula r v => relation M r (vmap (interpreted_term M assignment) v)
| negation f => ¬ satisfies M f assignment
| disjunction f1 f2 => satisfies M f1 assignment ∨ satisfies M f2 assignment
| conjunction f1 f2 => satisfies M f1 assignment ∧ satisfies M f2 assignment
| existence_quantor v f => ∃ i, satisfies M f (λ x, if v == x then i else assignment x)
| universal_quantor v f => ∀ i, satisfies M f (λ x, if v == x then i else assignment x)
end.
Structure Embedding Fm Rm Fn Rn (Lm: Language Fm Rm) (Ln: Language Fn Rn) (M: Structure Lm) (N: Structure Ln) := {
domain_map: domain M → domain N;
function_map: Fm → Fn;
relation_map: Rm → Rn;
function_arity_preserved: ∀ f, function_arity Lm f = function_arity Ln (function_map f);
relation_arity_preserved: ∀ r, relation_arity Lm r = relation_arity Ln (relation_map r);
embedding_function_property: ∀ f v, domain_map (function M f v) =
function N (function_map f) (vmap domain_map (rew [λ W, (domain M ^ W)%type] (function_arity_preserved f) in v));
embedding_relation_property: ∀ r v, relation M r v ↔
relation N (relation_map r) (vmap domain_map (rew [λ W, (domain M ^ W)%type] (relation_arity_preserved r) in v));
}.
Definition injective A B (f: A → B) := ∀ a b, f a = f b → a = b.
(* ?? *)
Definition embedding_is_substructure F R (L: Language F R) (M: Structure L) (N: Structure L) (E: Embedding M N) :=
injective (domain_map E) ∧ (∀ x, function_map E x = x) ∧ (∀ x, relation_map E x = x).
Definition quantifier_free_formula F R (V: eqType) (L: Language F R) (A: Formula V L): Prop :=
match A with
| existence_quantor v f => False
| universal_quantor v f => False
| _ => True
end.
Theorem T1_1_8 F R (V: eqType) (L: Language F R) (M N: Structure L) (E: Embedding M N)
(H0: embedding_is_substructure E) (assignment: V → domain M) (A: Formula V L) (H1: quantifier_free_formula A):
satisfies M A assignment ↔ satisfies N A (domain_map E \o assignment).
Proof.
destruct E. simpl in *. unfold embedding_is_substructure in H0. simpl in *. destruct H0. destruct H0.
unfold injective in H. induction A; simpl in *; split; intros.
+ apply embedding_relation_property0 in H3. rewrite (H2 r) in H3.
Admitted.
```

I don't know how to solve your problem, but note that since you imported `all_ssreflect`

, you are using the ssr tactics that overshadow the standard ones (sorry, I didn't realize this when I suggested you import everything). Thus, your `rewrite`

is actually the ssr rewrite. If you use the standard one with `rewrite-> (H2 r) in H3.`

, you get essentially the same error message, except that `_pattern_value_`

is named `r0`

instead. This makes me think that the words "`_pattern_value_`

" are ultimately irrelevant, you can read the error message by thinking of it as just some variable.

IIRC, _pattern_value_ abstracts over what rewrite is trying to replace

This seems a dependent typing problem: your rewrite is producing some ill-typed term, possibly as an intermediate state. Those aren't fun to debug.

Paolo Giarrusso said:

Those aren't fun to debug.

Yes, I start to see that. :(

The example from https://math-comp.github.io/htmldoc/mathcomp.ssreflect.finfun.html isn't working. More specifically, `tree_rect`

definition gives me error message `No assumption in (K n)`

. :(

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset Elimination Schemes.
Inductive tree := node n of tree ^ n.
Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1.
Example tree_step (K : tree -> Type) :=
forall n st (t := node st) & forall i : 'I_n, K (st i), K t.
Example tree_rect K (Kstep : tree_step K) : forall t, K t.
Proof. by fix IHt 1 => -n st; apply/Kstep=> i; apply: IHt. Defined.
```

since the example is commented out in `finfun.v`

, there is no reason to expect it to work (unmaintained code can break quickly)

Okay.

Got lucky and made it to work, it seems.

```
Example tree_rect K (Kstep : tree_step K) : forall t, K t.
Proof. exact (fix IHt t := match t with node n st => Kstep _ _ (fun i => IHt _) end). Defined.
```

Paolo Giarrusso said:

This seems a dependent typing problem: your rewrite is producing some ill-typed term, possibly as an intermediate state. Those aren't fun to debug.

It seems I have no idea how to debug this problem. :/ Do you have any hints or examples or something?

Thanks in advance.

Here is an example of what I think could be the same issue:

```
Goal forall T U (t : T) (H : T = U), t = t.
Proof.
intros T U t H.
Fail rewrite H.
(*
The command has indeed failed with message:
Abstracting over the term "T" leads to a term fun T0 : Type => t = t
which is ill-typed.
Reason is: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
"T0" : "Type"
"t" : "T"
"t" : "T"
The 2nd term has type "T" which should be coercible to
"T0".
*)
Abort.
```

(Note that if you import `ssreflect`

then the error message speaks about `_pattern_value_`

instead.)

I'm not confident in my understanding, but I think the issue is that we're trying to change the type of some term (`t`

in my example) without proving that `t : U`

. I have no idea how to solve this in general. Hopefully someone more knowledgeable can confirm my intuition and provide some solutions.

This works if you remove `t`

from the context: `move: t; rewrite H.`

(or `revert t; rewrite H`

)

@Lessness I have a fix!

First, I've tweaked the proof to make easier to read (no generated identifiers), and highlighted the problem. The first step of the rewrite produces an ill-typed term. Often, this means also the final step of the rewrite is ill-typed:

```
Theorem T1_1_8 F R (V: eqType) (L: Language F R) (M N: Structure L) (E: Embedding M N)
(ES: embedding_is_substructure E) (assignment: V → domain M) (A: Formula V L) (H1: quantifier_free_formula A):
satisfies M A assignment ↔ satisfies N A (domain_map E \o assignment).
Proof.
simpl in *; unfold embedding_is_substructure in ES; simpl in *.
destruct ES as [Hinj [HFunMap HRelMap]].
unfold injective in Hinj. induction A; simpl in *; split.
{ intros H. apply (embedding_relation_property E) in H.
revert H.
specialize (HRelMap r).
Fail rewrite HRelMap.
Fail generalize (relation_map E r).
(*
Error:
The command has indeed failed with message:
Illegal application:
The term "eq_rect" of type
"∀ (A : Type) (x : A) (P : A → Type), P x → ∀ y : A, x = y → P y"
cannot be applied to the terms
"nat" : "Set"
"relation_arity L r" : "nat"
"λ W : nat, (domain M ^ W)%type" : "nat → predArgType"
"vmap (interpreted_term M assignment) f"
: "(domain M ^ relation_arity L r)%type"
"relation_arity L r0" : "nat"
"relation_arity_preserved E r"
: "relation_arity L r = relation_arity L (relation_map E r)"
The 6th term has type
"relation_arity L r = relation_arity L (relation_map E r)"
which should be coercible to "relation_arity L r = relation_arity L r0".
*)
(*
F: Type
R: Type
V: eqType
L: Language F R
M, N: Structure L
E: Embedding M N
Hinj: ∀ a b : domain M, domain_map E a = domain_map E b → a = b
HFunMap: ∀ x : F, function_map E x = x
r: R
HRelMap: relation_map E r = r
assignment: V → domain M
f: Term V L ^ relation_arity L r
H1: True
====
relation N (relation_map E r)
(vmap (domain_map E)
(rew [λ W : nat, (domain M ^ W)%type] relation_arity_preserved E r in
vmap (interpreted_term M assignment) f))
→ relation N r (vmap (interpreted_term N (domain_map E \o assignment)) f)
*)
```

`eq_rect`

is the construct underlying the `rew`

notation — it uses equalities to cast across types.

hmm, still typing, but my fix is probably not the right one :-|

The problem is that your term uses:

```
relation_arity_preserved E r : relation_arity L r = relation_arity L (relation_map E r)
```

but the `rewrite`

tries to replace `relation_map E r`

by `r`

. however, it can't change the type of `relation_arity_preserved`

:-|

so, the problem is (a) the term you're trying to write doesn't typecheck (b) that's because you can't rewrite in the type of `relation_arity_preserved`

. Often, that's fixable by abstracting over the term containing the problem, or by rewriting only in some occurrences. In all cases, you need to think about how to get the program you want to typecheck...

One bad "fix" is to generalize over the entire problematic block. I use `move: term`

instead of `generalize term`

because the latter isn't working here:

```
move: (rew [λ W, (domain M ^ W)%type] relation_arity_preserved E r in
vmap (interpreted_term M assignment) f).
rewrite HRelMap.
```

But that throws away too much info. We can do a bit better this way:

```
generalize (relation_arity_preserved E r).
rewrite HRelMap.
```

We're left with:

```
∀ e : relation_arity L r = relation_arity L r,
relation N r
(vmap (domain_map E)
(rew [λ W : nat, (domain M ^ W)%type] e in
vmap (interpreted_term M assignment) f))
→ relation N r (vmap (interpreted_term N (domain_map E \o assignment)) f)
```

and here, `intros e. rewrite (eq_irrelevance e erefl). simpl. clear e.`

gets rid of the remaining problems AFAICT:

```
relation N r (vmap (domain_map E) (vmap (interpreted_term M assignment) f))
→ relation N r (vmap (interpreted_term N (domain_map E \o assignment)) f)
```

basically, we must show that `e`

is really Coq's `Logic.eq_refl`

, the constructor of `eq`

(written `erefl`

in math-comp; `eq_refl`

is something else).

That is an instance of proof irrelevance — in particular, proof irrelevance for equality, AKA axiom K, AKA UIP. That's not true in general! But it's true for all equality on types with decidable equality, like `nat`

:-)

and then `eq_rect`

/`rew`

applies to `erefl`

just simplifies away.

hmm, maybe it's just me, but using proof irrelevance and dependent pattern matching seems like a very niche use of MathComp/SSReflect.

wouldn't this work better in regular Coq + Stdpp (or similar)?

@Paolo Giarrusso Thank you very much!

@Karl Palmskog that sounds as hard :sweat_smile:

the usual strategies I know are to try avoiding dependent types (and I'm not sure how that'd look here), or to turn the propositional equalities into definitional ones

here, the problem is that an `Embedding`

must quantifies over _two_ languages `Lm`

and `Ln`

, and then assert propositionally that `Ln`

includes `Lm`

and preserves arities

If you can rewrite `Ln`

as `Lm + Lrest`

, and define `+`

, `function_arity`

and `relation_arity`

such that these equalities become propositional:

```
function_arity_preserved: ∀ f, function_arity Lm f = function_arity Ln (function_map f);
relation_arity_preserved: ∀ r, relation_arity Lm r = relation_arity Ln (relation_map r);
```

then you're golden.

But I don't have a successful strategy to teach for that, beyond reusing designs from Agda libraries or from Conor McBride!

the MathComp approach would probably be to leverage a boolean-based (decidable) definition of (preservation of) function arities and relation arities to encode the whole thing, which should supress the need for dependent types

I know the usual answer but I don't know how to apply it here

(1) how do you translate `Definition Function A n := A^n → A.`

?

(2) embedding-ness seems undecidable, because of properties like ```
embedding_function_property: ∀ f v, domain_map (function M f v) =
function N (function_map f) (vmap domain_map (rew [λ W, (domain M ^ W)%type] (function_arity_preserved f) in v));
```

AFAICT, that's an homomorphism property on potentially infinite domains — something like `hom (f args) = (hom f) (map hom args)`

so, wouldn't it be possible to restrict your domain(s) just enough to make it become decidable?

AFAICT, the proof is reasoning about two models of first-order logic. One can restrict to *finite* models — and maybe that's enough for @Lessness 's use-case — but that's a strictly *weaker* theorem.

sure, the same applies for any graph reasoning using MathComp's `fingraph`

for example, but in many cases it's still useful, and you get a big [productivity] boost from boolean rewriting/reduction + small scale reflection

looking at `fingroup.v`

, they avoid _these_ dependent types indeed, but AFAICT that's not because of decidability, but because they fixed a concrete `Language`

.

in particular, `Embedding`

combines (a) `Lm`

is a sublanguage of `Ln`

(b) `M`

lifted through the proof of (a) is a substructure of `N`

.

even if we make (a) decidable, the statement of (b) requires dealing with awkward dependent types. A nice general fix here might be a good induction principle for the sublanguage property, similar to the J induction axiom for equality: to prove lemma `T1_1_8`

in general, it suffices to prove it for the case where (a) is proved by (the analogue of "eq_refl" (the reflexivty sublanguage property)

But I'm speculating: I have _not_ seen this technique, and I don't know if it works out. If it does, it's probably folklore among HoTT people (even if nothing relies on HoTT here).

I got a problem in my formalization. The github repozitory is here: https://github.com/LessnessRandomness/Model-theory-in-Coq

I did some formalization of (very) basic model theory stuff (in file `basics.v`

). Then I started testing and found out that computation of `interpreted_term`

isn't working as it should (file `testing.v`

, line 73).

Maybe I made some obvious beginner's mistake... I don't know. I will keep looking for the solution myself too, of course.

I will try to minimize the code that contains the problem. I should have done that before posting about the problem, probably.

```
From mathcomp Require Import all_ssreflect.
Require Import Utf8.
Set Implicit Arguments.
Structure Language F := {
function_arity: F → nat;
}.
Definition Function A n := A^n → A.
Inductive Term {F} (V: eqType) (L: Language F) :=
| variable: V → Term V L
| function_term: ∀ (f: F), (Term V L)^(function_arity L f) → Term V L.
Structure Structure {F} (L: Language F) := {
domain: Type;
function: ∀ (f: F), Function domain (function_arity L f);
}.
Fixpoint interpreted_term F (V: eqType) (L: Language F) (M: Structure L) (assignment: V → domain M) (T: Term V L): domain M :=
match T with
| variable x => assignment x
| function_term f v => function M f (finfun (interpreted_term M assignment \o v))
end.
Inductive F := minus.
Definition L: Language F.
Proof.
refine (Build_Language _).
exact (λ f, match f with minus => 2 end).
Defined.
(* v1 *)
Definition t0: Term nat_eqType L := variable _ _ 1.
(* v3 - v1 *)
Definition t1: Term nat_eqType L.
Proof.
exact (function_term minus [ffun x => match nat_of_ord x with 0 => variable _ _ 3 | _ => variable _ _ 1 end]); clear x.
Defined.
Definition M: Structure L.
Proof.
refine (@Build_Structure _ L nat _).
intro f. set (ord0 (n':=1)) as ord0_2. set (Ordinal (ltac:(auto):(1<2))) as ord1_2.
refine (match f with minus => _ end); simpl.
intro v. exact (v ord0_2 - v ord1_2).
Defined.
Definition assignment: nat → nat := id.
Eval compute in (interpreted_term M assignment t0). (* computes *)
Eval compute in (interpreted_term M assignment t1). (* gets stuck *)
```

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Eval compute in (codom (finfun (@nat_of_ord 2))).
(* Should compute to [:: 0; 1]. Does not. *)
```

Ok, now I don't know what's going on.

`compute`

and performant Coq libraries, including math-comp, don't generally agree.

That's because of sealed definitions: They're analogues to `Definition x := body.`

, but ensure that `x`

does _not_ reduce to `body`

. That's annoying when computing on concrete values, but better otherwise. This question has come up before but I don't remember if there was a solution...

Could that be the problem here?

Thank you!

I don't know what to do now - to stay with MathComp, use Standard Library or maybe both variants simultaneously... I still want to learn MathComp, just a bit disappointed. :(

Some flag (or smth) in MathComp that allows computing for the specific situation, that would be very nice. One can dream. :|

Last updated: Nov 29 2023 at 04:01 UTC