The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Jeremy,

The thing "{| c := ccc ; i := iii |}" is record data type [1] and you can also think of it as inductive data type with one constructor.  I wrote a simple example, see below.

Require Import Coq.Strings.String.
Record person := mk_name
{
name : string;
age : nat
}.

Lemma identity : forall p q : person, p = q -> q = p.
Proof.
intros ? ? Hpq.
(*

p, q: person
Hpq: p = q
-----------------
1/1
q = p
*)

destruct q. destruct p.

(* The context looks like:
name1: string
age1: nat
name0: string
age0: nat
Hpq: {| name := name1; age := age1 |} = {| name := name0; age := age0 |}
------------------------------------------------------------------------
1/1
{| name := name0; age := age0 |} = {| name := name1; age := age1 |}
*)

inversion Hpq. (* get the equality between the corresponding fields *)

(*
name1: string
age1: nat
name0: string
age0: nat
Hpq: {| name := name1; age := age1 |} = {| name := name0; age := age0 |}
H0: name1 = name0
H1: age1 = age0
--------------------------------------------------------------------------
1/1
{| name := name0; age := age0 |} = {| name := name0; age := age0 |}
*)
reflexivity.
Qed.

" If so how do I actually get hold of those things?"

You can access the individual field by using the corresponding field names, e.g., if you have a person p, then you can access its name by (name p) and age by (age p). 

"Then, when I have a goal of the form {| c := ccc ; i := iii |} what does that mean and what is the next step to solving it?" 

When we have a goal, say, of A (Type, Set, or Prop), then we need to produce a witness of A. For example, in the example below,

I am producing a person as a return type, and I can do that in many ways. I can just return p, or I can construct any  arbitrary person

by using the constructor 'mk_name'.

Theorem identity_function : forall p: person, person.
Proof.
intros p.

(* see the type of pn and qn *)
remember (name p ) as pn.
remember (age p) as qn.

exact ( {| name := name(p); age := age(p) |}).
(*
you can write 'exact p' or  you can provide it using the constructor
exact (mk_name EmptyString 10).
*)
Defined.

However, in your case, I believe, it will be type error because {| c := ccc ; i := iii |} is not of  Type, Set, or Prop.


Best,
Mukesh




[1] https://coq.inria.fr/refman/language/core/records.html

On Mon, Sep 6, 2021 at 12:25 PM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi,

I have a hypothesis (got by playing around with someone else's code) of
the form {| c := ccc ; i := iii |}

The command Locate "{|". produces no results.

I found in the documentation a syntax definition

term_record::={| field_def*; ;? |}

but I can't find anything about what that means or what you can do with it.

Does it mean I have a thing of type ccc and another thing of type iii?

If so how do I actually get hold of those things?

Then, when I have a goal of the form {| c := ccc ; i := iii |}
what does that mean and what is the next step to solving it?

Thanks

Jeremy