dependent.v

Variable A:Set.

Inductive Vec : nat -> Set:=
  | VNil : Vec 0
  | VCons : forall n, A -> Vec n -> Vec (S n).

Print Vec.

Inductive bool := | true | false.

Inductive Vecb : nat -> Set :=
  | VbNil : Vecb 0
  | VbCons : forall n, bool -> Vecb n -> Vecb (S n).

Print Vecb.

Definition head n : Vecb (S n) -> bool.
  intros.
  inversion H. exact H1.
Defined.

Print head.

Eval compute in (VbCons 0 true VbNil).
Eval compute in (VbCons 1 true (VbCons 0 true VbNil)).

Definition ex1 := (VbCons 1 true (VbCons 0 true VbNil)).

Print ex1.
Eval compute in (head 1 ex1).
  (* 上記headの定義でQedとするとここで計算してくれない *)

Definition inner_prod n : Vecb n -> Vecb n -> bool.
  intros.
  exact true. Qed.

Print inner_prod.

(* http://yosh.hateblo.jp/entry/20080714/p1 *)

Definition head_qed n : Vecb (S n) -> bool.
  intros.
  inversion H. exact H1.
Qed.

Eval compute in (head_qed 1 ex1).

(* Transparent head_qed. *)

Opaque head.
Eval compute in (head 1 ex1).
Transparent head.
Eval compute in (head 1 ex1).

Print head.
Check ex1.

Definition head_def n (v: Vecb (S n)) : bool := match v with
  |  VbNil => false
  |  VbCons _ b  _ => b
end.

Theorem head1 : head 1 ex1 = head_def 1 ex1.
Proof.
simpl. reflexivity. Qed.

Theorem head_equiv1 : forall n v b, 
   head n (VbCons n b v) = head_def n (VbCons n b v).
Proof.
  intros.
  simpl. reflexivity. Qed.

Theorem head_equiv : forall n v, 
   head n v = head_def n v.
Proof.
  intros.
  refine (match v with VbNil => _ | VbCons n b v=> _ end ).
  exact id.
  simpl. reflexivity. Qed.

Print head_equiv.