How do I prove a record related lemma?

Question

I'm new to coq. I would appreciate it if you could help me.

Consider the following definition:

Record person:= mk_person { p_name : t1; p_age : t2}.

How to prove the following lemma?

Lemma person_lemma : forall (p:person)(name:t1)(age:t2), 
    p_name p = name ->
    p_age  p = age  ->
    p ={|p_name := name; p_age := age|}.

Welcome to PASE! It would be nice if you can share your own effort and what problems you have encountered. You have given examples using some types like t1, t2 which are not defined in your question. It is easier to get people to help you if you provide these background information. — ice1000, Commented Dec 7, 2022 at 8:10
I'm voting to keep this open, not just because this is a brand new user, but also because an answer was already given (the question does not "need details for clarity", which was the currently proposed close reason). — Nike Dattani, Commented Jan 2, 2023 at 6:37
@NikeDattani It still needs detail. Where exactly is the difficulty? Where is the OP stuck? We need to know that in order to give helpful answers. — Trebor, Commented Jan 4, 2023 at 8:18
@NikeDattani I'm not voting because my decisions would be final. But having an answer doesn't really affect the close reasons. — Trebor, Commented Jan 4, 2023 at 13:40

Pierre Courtieu · Accepted Answer · 2022-12-07 09:42:36Z

Remember that a records is syntactic sugar for an inductive with one constructor. Your record is mostly equivalent to:

Inductive person:= mk_person: forall(p_name : t1)(p_age : t2), person.

and the projection functions:

Definition p_name (p:person) := let '(mk_person name _) := p in name.
Definition p_age (p:person) := let '(mk_person _ age) := p in age.

One difference is that this way you don't have the `{| ... |} notation, so the lemma would be rephrased like this:

Lemma person_lemma : forall (p:person)(name:t1)(age:t2), 
    p_name p = name ->
    p_age  p = age  ->
    p = mk_person name age.

If you know to prove this lemma, then the same script should work for the record:

  intros p name age H H0. 
  destruct p.
  now subst.

1 Answer 1