The Coq mailing list

[Madhukar <madhukar.yerraguntla AT gmail.com>]

Hi Jeremy,

As Agnishom mentioned, records are nothing special. If you are familiar with Haskell or ocaml, the record fields can be accessed similarly. For example:

Record test := mk_test {

name : string;

val : nat}.

Fixpoint test_find (n: string) (xl: list test) : option test :=

match xl with

| [] => None

| x::xs => if (String.eqb (name x) n) then Some x else test_find n xs

end.

(*This uses the haskell-like syntax to refer to name field*)

Fixpoint test_find2 (n: string) (xl: list test) : option test :=

match xl with

| [] => None

| x::xs => if (String.eqb x.(name) n) then Some x else test_find n xs

end.

(* This uses ocaml-like syntax. The peculiarity is the parentheses which are required to parse the statement correctly *)

Lemma test_correct: forall xl n x, test_find n xl = Some x -> x.(name) = n.

Proof.

induction xl; intros; simpl in *.

- inversion H.

- unfold test_find. destruct (name a =? n) eqn:E.

* inversion H; subst x. now apply String.eqb_eq in E.

* now apply IHxl.

Qed.

Thanks,

Madhukar

 

On Mon, Sep 6, 2021 at 9:40 AM Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

I apologize. Here is a more syntactically correct example.

Inductive Rectangle : Type := {
  height : nat;
  width : nat;
  }.
 
 
Example foo_rect := {| height := 4; width := 5 |}.

Print foo_rect.
Check foo_rect.

Does this help understand what Record types are?

As for your goal, could you give a minimal complete example of the problem you are facing? I could not come up with a natural example myself.

On Sun, Sep 5, 2021 at 10:59 PM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi Agnishom,

I'm rather puzzled - I assume you are saying that the syntax I gave, ie
{| c := ccc ; i := iii |}, is in fact a record.

But if so, why doesn't the split tactic work?

The following you gave:

Definition Person : Type := {
    name : String;
    age : int;
}.

I'm guessing you are saying that defines a record type in Coq.

However why I enter that I get the following error:

Definition Person : Type := {
   name : String;
   age : intCoq < Coq < Coq < }.
Toplevel input, characters 46-47:
 >   name : String;
 >                ^
Error:
Syntax error: '&' or '|' expected after [constr:operconstr level 200]
(in [constr:operconstr]).

Cheers,

Jeremy


On 6/9/21 1:32 pm, Agnishom Chattopadhyay wrote:
> Records are like a product type, with desginated function for each
> projection function. Informally, you can think of them as a class with
> fields in some object oriented language.
>
> For example,
>
> class Person {
>    String name;
>    int age;
> }
>
> would be
>
> Definition Person : Type := {
>    name : String;
>    age : int;
> }.
>
> You can read the section titled "Records are Products" from
> https://softwarefoundations.cis.upenn.edu/qc-current/Typeclasses.html
> <https://softwarefoundations.cis.upenn.edu/qc-current/Typeclasses.html>
> (The rest of the page is not really relevant for this purpose.)
>
> Records are also a feature in OCaml or Haskell. You can google that.
>
>
>
> On Sun, Sep 5, 2021 at 10:20 PM Agnishom Chattopadhyay
> <agnishom AT cmi.ac.in <mailto:agnishom AT cmi.ac.in>> wrote:
>
>     Locate locates notation that is defined by the programmer. I believe
>     that "{|" is syntax which is part of Gallina.
>
>     As for the next step, have you tried split? You can also try solving
>     this with exact.
>
>     --agnishom
>
>     On Sun, Sep 5, 2021, 21:25 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au
>     <mailto: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
>