The Coq mailing list

[Christina Peterson <clp8199 AT knights.ucf.edu>]

Hello,

I am working with a record in the Coq Proof Assistant and would like to be able to access and display elements of the record in the proof environment so that I can apply formal logic to them. I have attached the file Example.v which is a simple reproducible example of the problem.

Sincerely,

Christina

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Record program : Type := mkprogram {
  prog_defs: list nat
}.

Definition program1 :=
mkprogram (1::2::3::4::nil).

Definition func_program(x:program) :=
  match x with
  | _ => x.(prog_defs)
  end.

Definition head (default:nat) (l: list nat) : nat :=
  match l with
  | nil => default
  | h :: t => h
  end.

(*Definition prog_const := program -> Prop.

Example example_proof :
  forall c: prog_const,
  c program1.
Proof.
*)

(* This example shows that the head of the list is 1 *)

Example list_head :
  head 0 (func_program program1) = 1.
Proof.
  unfold func_program. unfold prog_defs.
  (*This is the point where I want to visually see the
    list 1::2::3::4::nil*) 
  reflexivity. Qed.

(*As you can see, it is possible to complete the proof without 
visually showing the list. However, when proving properties of 
more complex examples, it is helpful to visually display the 
data stored in the record field*)