Lessness (Jul 18 2022 at 11:37): Lessness (Jul 18 2022 at 11:37):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.
Karl Palmskog (Jul 18 2022 at 11:40):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
Ana de Almeida Borges (Jul 18 2022 at 14:09):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.
Lessness (Jul 18 2022 at 14:39):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.
Pierre Castéran (Jul 18 2022 at 14:49):The PnP book https://ilyasergey.net/pnp/pnp.pdf may be useful for learning quietly ssreflect ...
Lessness (Jul 18 2022 at 15:37):A question... is there something like map and also fold_right that works on T^n?
Karl Palmskog (Jul 18 2022 at 15:46):use canonical big operators: https://www-sop.inria.fr/marelle/bigops/main.pdf
Lessness (Jul 18 2022 at 15:48):Thank you!
Lessness (Jul 18 2022 at 16:49):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
Lessness (Jul 18 2022 at 17:10):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.
Alexander Gryzlov (Jul 18 2022 at 22:00):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) .. )
Lessness (Jul 19 2022 at 04:53):Thank you!
Lessness (Jul 19 2022 at 05:38):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))
Paolo Giarrusso (Jul 19 2022 at 09:01):What stdlib types are idiomatic to use in ssreflect?
Karl Palmskog (Jul 19 2022 at 09:09):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"
Karl Palmskog (Jul 19 2022 at 09:10):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
Karl Palmskog (Jul 19 2022 at 09:11):but I think there are some sigma types and other similar things are used in MathComp, but sparingly
Lessness (Jul 19 2022 at 13:57):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 (Jul 19 2022 at 14:01):Lessness said:
When I tried to make analogue of
Forallusing bigop (like infold_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?
Karl Palmskog (Jul 19 2022 at 14:03):the closest to \in for lists is arguably: https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html#in_dec
Ana de Almeida Borges (Jul 19 2022 at 14:12):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.
Lessness (Jul 19 2022 at 14:18):Ana de Almeida Borges said:
For lists with a fixed size there is the mathcomp
tuple, and for lists of bounded size you can findbseqin 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.
Ana de Almeida Borges (Jul 19 2022 at 14:21):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.
Ana de Almeida Borges (Jul 19 2022 at 14:43):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.
Lessness (Jul 20 2022 at 11:32):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_?
Ana de Almeida Borges (Jul 21 2022 at 15:30):I've never seen that. Feel free to post the code.
Lessness (Jul 21 2022 at 15:33):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.
Paolo Giarrusso (Jul 21 2022 at 18:37):IIRC, _pattern_value_ abstracts over what rewrite is trying to replace
Paolo Giarrusso (Jul 21 2022 at 18:40):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.
Lessness (Jul 21 2022 at 19:49):Paolo Giarrusso said:
Those aren't fun to debug.
Yes, I start to see that. :(
Lessness (Jul 21 2022 at 21:42):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)
Lessness (Jul 21 2022 at 21:53):Okay.
Lessness (Jul 21 2022 at 22:09):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.
Ana de Almeida Borges (Jul 22 2022 at 16:57):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.)
Ana de Almeida Borges (Jul 22 2022 at 17:00):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.
Alexander Gryzlov (Jul 22 2022 at 17:24):This works if you remove t from the context: move: t; rewrite H.
Alexander Gryzlov (Jul 22 2022 at 17:26):(or revert t; rewrite H)
Paolo Giarrusso (Jul 22 2022 at 18:28):@Lessness I have a fix!
Paolo Giarrusso (Jul 22 2022 at 18:30):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.
Paolo Giarrusso (Jul 22 2022 at 18:34):hmm, still typing, but my fix is probably not the right one :-|
Paolo Giarrusso (Jul 22 2022 at 18:35):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 :-|
Paolo Giarrusso (Jul 22 2022 at 18:38):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).
Paolo Giarrusso (Jul 22 2022 at 18:44):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 :-)
Paolo Giarrusso (Jul 22 2022 at 18:45):and then eq_rect/rew applies to erefl just simplifies away.
Karl Palmskog (Jul 22 2022 at 18:48):hmm, maybe it's just me, but using proof irrelevance and dependent pattern matching seems like a very niche use of MathComp/SSReflect.
Karl Palmskog (Jul 22 2022 at 18:49):wouldn't this work better in regular Coq + Stdpp (or similar)?
Lessness (Jul 22 2022 at 18:49):@Paolo Giarrusso Thank you very much!
Paolo Giarrusso (Jul 22 2022 at 18:50):@Karl Palmskog that sounds as hard :sweat_smile:
Paolo Giarrusso (Jul 22 2022 at 18:51):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
Paolo Giarrusso (Jul 22 2022 at 18:52):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
Paolo Giarrusso (Jul 22 2022 at 18:53):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.
Paolo Giarrusso (Jul 22 2022 at 18:54):But I don't have a successful strategy to teach for that, beyond reusing designs from Agda libraries or from Conor McBride!
Karl Palmskog (Jul 22 2022 at 20:26):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
Paolo Giarrusso (Jul 22 2022 at 20:51):I know the usual answer but I don't know how to apply it here
Paolo Giarrusso (Jul 22 2022 at 20:53):(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));
Paolo Giarrusso (Jul 22 2022 at 20:56):AFAICT, that's an homomorphism property on potentially infinite domains — something like hom (f args) = (hom f) (map hom args)
Karl Palmskog (Jul 22 2022 at 21:09):so, wouldn't it be possible to restrict your domain(s) just enough to make it become decidable?
Paolo Giarrusso (Jul 22 2022 at 21:15):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.
Karl Palmskog (Jul 22 2022 at 21:21):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
Paolo Giarrusso (Jul 22 2022 at 21:22):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.
Paolo Giarrusso (Jul 22 2022 at 21:24):in particular, Embedding combines (a) Lm is a sublanguage of Ln (b) M lifted through the proof of (a) is a substructure of N.
Paolo Giarrusso (Jul 22 2022 at 21:29):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)
Paolo Giarrusso (Jul 22 2022 at 21:30):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).
Lessness (Jul 26 2022 at 19:24):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.
Lessness (Jul 26 2022 at 19:58):I will try to minimize the code that contains the problem. I should have done that before posting about the problem, probably.
Lessness (Jul 26 2022 at 20:11):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.
Paolo Giarrusso (Jul 27 2022 at 03:00):compute and performant Coq libraries, including math-comp, don't generally agree.
Paolo Giarrusso (Jul 27 2022 at 03:03):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...
Paolo Giarrusso (Jul 27 2022 at 03:04):Could that be the problem here?
Paolo Giarrusso (Jul 27 2022 at 11:38): Lessness (Jul 27 2022 at 14:57):Thank you!
Lessness (Jul 27 2022 at 19:29):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: Apr 20 2024 at 07:01 UTC