Stream: Coq users

Topic: Type-Checking field of records

Roberto Cebulski (Apr 30 2021 at 19:19):

Hello everyone, new around here, glad to be here.
Suppose I have a record,
Record foo :=
{tp:Type; coloftpprop:(tp -> Prop) -> Prop}.
and two foos , foo1 and foo2 and a proof of (tp foo1 = tp foo2). How can I make this definition type check?
Definition fooimpfoo (foo1 foo2:foo) :=
forall fp, (coloftp foo1) fp -> (coloftp foo2) fp.
The error i'm given is:
Error:
In environment
foo1 : foo
foo2 : foo
fp : tp foo1 -> Prop
The term "fp" has type "tp foo1 -> Prop" while it is expected to have type
"tp foo2 -> Prop" (cannot unify "tp foo2" and "tp foo1").

Paolo Giarrusso (Apr 30 2021 at 19:38):

you need to use explicitly the equality. For instance, something like:

Definition fooimpfoo (foo1 foo2:foo).
Proof.
  refine (forall fp, (coloftp foo1) fp -> (coloftp foo2) _).
  rewrite <-your_equality.
  exact fp.
Defined.

Paolo Giarrusso (Apr 30 2021 at 19:40):

I didn't try it out in Coq, but I hope it gives the idea — feel free to ask question.

Paolo Giarrusso (Apr 30 2021 at 19:41):

One can also write the proof term by hand, but I feel that's more advanced (I'd have to look it up).

Roberto Cebulski (Apr 30 2021 at 19:44):

Thank you very much, I made it work by :
Definition fooimpfoo (foo1 foo2:foo) (p:tp foo1 = tp foo2):Prop.
Proof.
refine (forall fp, (coloftp foo1) fp -> (coloftp foo2) _).
rewrite <-p.
exact fp.
Defined.

Last updated: Sep 25 2023 at 12:01 UTC