Proof mode definitions in Coq?

Question

Can anyone give me some good source on how to read proof mode-definitions (an example is given:)

Definition A (ss: FSS) (n:nat)
             (s: {s:S | state_is_wf s
                            /\ RESS.get_element n (proj1_sig ss) = Some s})
    : FS.
    destruct s. destruct a.
    refine (exist _ x _).
    apply H.
  Defined.

where 'FSS', 'FS' and 'S' are sig types defined earlier. I know what the inidividual tactics 'destruct', 'refine' and 'apply' do, but in a proof term for a definition, I can't read this proof without probably compiling (I cannot compile these files, can only read their source code.) Can anyone either help me with how to read such definitions or point me to some source?

Guillaume Melquiond Guillaume Melquiond · Accepted Answer · 2020-08-28T06:14:47

Without compiling the definition (and without seeing the definitions of FS and FSS), it is impossible, but we can still guess a bit. The destruct tactic creates a match with construct on s, which is of type sig, which has a unique constructor exist. There is no a among the arguments of the function, so a is either a global symbol, or it is a variable created by the first destruct. Let us assume it is the latter. Same thing for x.

Tactic refine creates a term, possibly with holes. Term exist _ x _ contains two holes. The first _ is filled by Coq, but the last one presumably has to be filled by the user, so that is what apply H is for. As for H, let us assume it comes from one of the previous destruct.

Note that apply might first decompose inductive values with only one constructor. So, if H happens to be of type A /\ B (which it would be if it comes from the first destruct), apply H might actually be apply (proj1 H) or apply (proj2 H). Anyway, since the proof is now finished, this apply is presumably exact.

So, there are numerous possibilities. Here is an example:

Definition A ss n s :=
  match s with
  | exist _ a H =>
    match a with
    | ... x ... =>         (* H could come from there too *)
      exist _ x (proj1 H)  (* or (proj2 H), or plain H *)
    end
  end.

Proof mode definitions in Coq?

1 Answers