walker (Oct 28 2022 at 07:51): walker (Oct 28 2022 at 07:51):Consider the following example:
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Module EQ.
Record class (T: Type) := Class {cmp: T -> T -> bool}.
Structure type := Pack{obj: Type; class_of: class obj}.
Definition op (e: type): obj e -> obj e -> bool :=
let 'Pack (Class the_cmp) := e in the_cmp.
Arguments op {e} x y : simpl never.
Arguments Class {T} cmp.
Module theory.
Notation "x == y" := (op x y) (at level 70).
End theory.
End EQ.
Import EQ.theory.
Fixpoint nat_eq x y :=
match x, y with
| O, O => true
| S x', S y' => nat_eq x' y'
| _, _ => false
end.
Canonical Structure nat_eq_ty : EQ.type.
Proof.
(*econstructor works*)
I want a way nicer than econstructor and apply .. with that kind of unfolds EQ.type Imagine I have like 20~30 lemmas to prove how can I do it nicely with tactics language.
walker (Oct 28 2022 at 07:52):what I want to do is to solve all the goals one by one instead of having to do a very long apply ... with ...
Gaëtan Gilbert (Oct 28 2022 at 07:54):please explain more what's wrong with econstructor
walker (Oct 28 2022 at 07:58):nothing is wrong with econstructor by I have intuition that econstructor is mostly for testing/prototyping and it is not final solutions. but I can be wrong.
Enrico Tassi (Oct 28 2022 at 08:33):The question is not CS specific, please retitle
walker (Oct 28 2022 at 09:53):I am not sure I am following what you are trying to say
Paolo Giarrusso (Oct 28 2022 at 10:11):I'm not sure you want to define CSes using tactics (beyond prototyping); math-comp's pattern never does it. In qed proofs, econstructor or eapply are options, but ssreflect tactics like apply: or apply/ work better with CSes (they use a different unification algorithm)
Michael Soegtrop (Oct 28 2022 at 10:55):What I typically do when I want to define a record which has 20..30 lemmas is to create a module where each lemma is in and then just fill in the names in the record definition.
walker (Oct 28 2022 at 10:59):Apparently I couldn't do it with econstructor either,
at Qed coq complained about something broken,
@Michael Soegtrop
I see, I thought it might be a bit more intuitive that to prove the record instead but I might have to do it the way you described.
Kenji Maillard (Oct 28 2022 at 11:13):econstructor might shelve some goals (= keeping them aside in the hope that they are automatically solved by unification when closing another goal). A pattern that I sometimes use is the combination unshelve econstructor to obtain all the created goals and not leave any on the shelf.
You can also bypass econstructor entirely and apply the constructor of your choice, in your case Eq.Pack (yes it does depends on knowing the record you want to build, but that sounds reasonable when you want to inhabit that record type).
walker (Oct 28 2022 at 12:29):unshelve econstructor, almost works!
Canonical Structure foo : EQ.type.
Proof.
unshelve econstructor.
- apply nat.
- constructor.
apply nat_eq.
Qed.
gives the following error:
Could not declare a canonical structure foo.
Could not find its value in the global environment.
No more subgoals.
But I figured that I can just put everything in the record class and that will be the thing that is populated
Paolo Giarrusso (Oct 28 2022 at 12:59):I think Qed is not correct here, you'd need Defined: Qed means Coq can't even find or run your nat_eq function
Paolo Giarrusso (Oct 28 2022 at 12:59):I wonder if that explains those errors
walker (Oct 28 2022 at 13:01):yeah it makes perfect sence, I forgot that this case Qed is not good, I thought maybe there is a deep hidden reason.
Last updated: Sep 23 2023 at 14:01 UTC