Library GenModel
A general model construction of a model of CC given an
abstract model.
Module MakeModel(M : CC_Model).
Import M.
Lemma eq_fun_sym : ∀ x f1 f2, eq_fun x f1 f2 -> eq_fun x f2 f1.
Lemma eq_fun_trans : ∀ x f1 f2 f3,
eq_fun x f1 f2 -> eq_fun x f2 f3 -> eq_fun x f1 f3.
Valuations
Module Xeq.
Definition t := X.
Definition eq := eqX.
Definition eq_equiv : Equivalence eq := eqX_equiv.
End Xeq.
Require Import VarMap.
Module V := VarMap.Make(Xeq).
Notation val := V.map.
Notation eq_val := V.eq_map.
Definition vnil : val := V.nil props.
Import V.
Hint Unfold eq_val.
Definition t := X.
Definition eq := eqX.
Definition eq_equiv : Equivalence eq := eqX_equiv.
End Xeq.
Require Import VarMap.
Module V := VarMap.Make(Xeq).
Notation val := V.map.
Notation eq_val := V.eq_map.
Definition vnil : val := V.nil props.
Import V.
Hint Unfold eq_val.
Module T.
Definition term :=
option {f:val -> X|Proper (eq_val ==> eqX) f}.
Definition eq_term (x y:term) :=
match x, y with
| Some f, Some g => (eq_val ==> eqX)%signature (proj1_sig f) (proj1_sig g)
| None, None => True
| _, _ => False
end.
Global Instance eq_term_refl : Reflexive eq_term.
Qed.
Global Instance eq_term_sym : Symmetric eq_term.
Qed.
Global Instance eq_term_trans : Transitive eq_term.
Qed.
Denotation as value
Definition int (t:term) (i:val) : X :=
match t with
| Some f => proj1_sig f (fun k => i k)
| None => props
end.
Global Instance int_morph : Proper (eq_term ==> eq_val ==> eqX) int.
Qed.
match t with
| Some f => proj1_sig f (fun k => i k)
| None => props
end.
Global Instance int_morph : Proper (eq_term ==> eq_val ==> eqX) int.
Qed.
Denotation as type
Definition el (t:term) (i:val) (x:X) :=
match t with
| Some _ => x ∈ int t i
| None => True
end.
Global Instance el_morph : Proper (eq_term ==> eq_val ==> eqX ==> iff) el.
Qed.
Lemma in_int_el : ∀ i x T,
x ∈ int T i -> el T i x.
match t with
| Some _ => x ∈ int t i
| None => True
end.
Global Instance el_morph : Proper (eq_term ==> eq_val ==> eqX ==> iff) el.
Qed.
Lemma in_int_el : ∀ i x T,
x ∈ int T i -> el T i x.
Injecting sets into the model
Syntax of the Calculus of Constructions
Definition prop := cst props.
Definition kind : term := None.
Definition Ref (n:nat) : term.
left; exists (fun i => i n).
Defined.
Definition App (u v:term) : term.
left; exists (fun i => app (int u i) (int v i)).
Defined.
Global Instance App_morph : Proper (eq_term ==> eq_term ==> eq_term) App.
Qed.
Definition Abs (A M:term) : term.
left; exists (fun i => lam (int A i) (fun x => int M (V.cons x i))).
Defined.
Global Instance Abs_morph : Proper (eq_term ==> eq_term ==> eq_term) Abs.
Qed.
Definition Prod (A B:term) : term.
left; exists (fun i => prod (int A i) (fun x => int B (V.cons x i))).
Defined.
Global Instance Prod_morph : Proper (eq_term ==> eq_term ==> eq_term) Prod.
Qed.
Definition kind : term := None.
Definition Ref (n:nat) : term.
left; exists (fun i => i n).
Defined.
Definition App (u v:term) : term.
left; exists (fun i => app (int u i) (int v i)).
Defined.
Global Instance App_morph : Proper (eq_term ==> eq_term ==> eq_term) App.
Qed.
Definition Abs (A M:term) : term.
left; exists (fun i => lam (int A i) (fun x => int M (V.cons x i))).
Defined.
Global Instance Abs_morph : Proper (eq_term ==> eq_term ==> eq_term) Abs.
Qed.
Definition Prod (A B:term) : term.
left; exists (fun i => prod (int A i) (fun x => int B (V.cons x i))).
Defined.
Global Instance Prod_morph : Proper (eq_term ==> eq_term ==> eq_term) Prod.
Qed.
Relocations
Section Lift.
Definition lift_rec (n m:nat) (t:term) : term.
destruct t as [(t,tm)|]; [left|exact kind].
exists (fun i => t (V.lams m (V.shift n) i)).
Defined.
Global Instance lift_rec_morph n k : Proper (eq_term ==> eq_term) (lift_rec n k).
Qed.
Definition lift1 n := lift_rec n 1.
Lemma lift10: ∀ T, eq_term (lift1 0 T) T.
Lemma int_lift_rec_eq : ∀ n k T i,
int (lift_rec n k T) i == int T (V.lams k (V.shift n) i).
Definition lift n := lift_rec n 0.
Global Instance lift_morph : ∀ k, Proper (eq_term ==> eq_term) (lift k).
Qed.
Lemma lift0_term : ∀ T, eq_term (lift 0 T) T.
Lemma simpl_int_lift : ∀ i n x T,
int (lift (S n) T) (V.cons x i) == int (lift n T) i.
Lemma simpl_int_lift1 : ∀ i x T,
int (lift 1 T) (V.cons x i) == int T i.
Lemma simpl_lift1 : ∀ i n x y T,
int (lift1 (S n) T) (V.cons x (V.cons y i)) == int (lift1 n T) (V.cons x i).
Lemma eqterm_lift_cst : ∀ n k c,
eq_term (lift_rec n k (cst c)) (cst c).
Lemma eq_lift_abs : ∀ n A B k,
eq_term (lift_rec n k (Abs A B))
(Abs (lift_rec n k A) (lift_rec n (S k) B)).
Lemma eq_lift_prod : ∀ n A B k,
eq_term (lift_rec n k (Prod A B))
(Prod (lift_rec n k A) (lift_rec n (S k) B)).
End Lift.
Definition lift_rec (n m:nat) (t:term) : term.
destruct t as [(t,tm)|]; [left|exact kind].
exists (fun i => t (V.lams m (V.shift n) i)).
Defined.
Global Instance lift_rec_morph n k : Proper (eq_term ==> eq_term) (lift_rec n k).
Qed.
Definition lift1 n := lift_rec n 1.
Lemma lift10: ∀ T, eq_term (lift1 0 T) T.
Lemma int_lift_rec_eq : ∀ n k T i,
int (lift_rec n k T) i == int T (V.lams k (V.shift n) i).
Definition lift n := lift_rec n 0.
Global Instance lift_morph : ∀ k, Proper (eq_term ==> eq_term) (lift k).
Qed.
Lemma lift0_term : ∀ T, eq_term (lift 0 T) T.
Lemma simpl_int_lift : ∀ i n x T,
int (lift (S n) T) (V.cons x i) == int (lift n T) i.
Lemma simpl_int_lift1 : ∀ i x T,
int (lift 1 T) (V.cons x i) == int T i.
Lemma simpl_lift1 : ∀ i n x y T,
int (lift1 (S n) T) (V.cons x (V.cons y i)) == int (lift1 n T) (V.cons x i).
Lemma eqterm_lift_cst : ∀ n k c,
eq_term (lift_rec n k (cst c)) (cst c).
Lemma eq_lift_abs : ∀ n A B k,
eq_term (lift_rec n k (Abs A B))
(Abs (lift_rec n k A) (lift_rec n (S k) B)).
Lemma eq_lift_prod : ∀ n A B k,
eq_term (lift_rec n k (Prod A B))
(Prod (lift_rec n k A) (lift_rec n (S k) B)).
End Lift.
Substitution
Section Substitution.
Definition subst_rec (arg:term) (m:nat) (t:term) : term.
destruct t as [(body,bm)|]; [left|right].
exists (fun i => body (V.lams m (V.cons (int arg (V.shift m i))) i)).
Defined.
Global Instance subst_rec_morph : Proper (eq_term ==> eq ==> eq_term ==> eq_term) subst_rec.
Qed.
Lemma int_subst_rec_eq : ∀ arg k T i,
int (subst_rec arg k T) i == int T (V.lams k (V.cons (int arg (V.shift k i))) i).
Definition subst arg := subst_rec arg 0.
Global Instance subst_morph : Proper (eq_term ==> eq_term ==> eq_term) subst.
Qed.
Lemma int_subst_eq : ∀ N M i,
int (subst N M) i == int M (V.cons (int N i) i).
Lemma el_subst_eq : ∀ N M i x,
el (subst N M) i x <-> el M (V.cons (int N i) i) x.
Lemma eqterm_subst_App : ∀ N u v,
eq_term (subst N (App u v)) (App (subst N u) (subst N v)).
Lemma eq_subst_prod : ∀ u A B k,
eq_term (subst_rec u k (Prod A B))
(Prod (subst_rec u k A) (subst_rec u (S k) B)).
End Substitution.
End T.
Import T.
Definition subst_rec (arg:term) (m:nat) (t:term) : term.
destruct t as [(body,bm)|]; [left|right].
exists (fun i => body (V.lams m (V.cons (int arg (V.shift m i))) i)).
Defined.
Global Instance subst_rec_morph : Proper (eq_term ==> eq ==> eq_term ==> eq_term) subst_rec.
Qed.
Lemma int_subst_rec_eq : ∀ arg k T i,
int (subst_rec arg k T) i == int T (V.lams k (V.cons (int arg (V.shift k i))) i).
Definition subst arg := subst_rec arg 0.
Global Instance subst_morph : Proper (eq_term ==> eq_term ==> eq_term) subst.
Qed.
Lemma int_subst_eq : ∀ N M i,
int (subst N M) i == int M (V.cons (int N i) i).
Lemma el_subst_eq : ∀ N M i x,
el (subst N M) i x <-> el M (V.cons (int N i) i) x.
Lemma eqterm_subst_App : ∀ N u v,
eq_term (subst N (App u v)) (App (subst N u) (subst N v)).
Lemma eq_subst_prod : ∀ u A B k,
eq_term (subst_rec u k (Prod A B))
(Prod (subst_rec u k A) (subst_rec u (S k) B)).
End Substitution.
End T.
Import T.
Definition env := list term.
Definition val_ok (e:env) (i:val) :=
∀ n T, nth_error e n = value T -> el (lift (S n) T) i (i n).
Lemma vcons_add_var0 : ∀ e T i x,
val_ok e i -> el T i x -> val_ok (T::e) (V.cons x i).
Lemma vcons_add_var : ∀ e T i x,
val_ok e i -> x ∈ int T i -> val_ok (T::e) (V.cons x i).
Lemma add_var_eq_fun : ∀ T U U' i,
(∀ x, el T i x -> int U (V.cons x i) == int U' (V.cons x i)) ->
eq_fun (int T i)
(fun x => int U (V.cons x i))
(fun x => int U' (V.cons x i)).
Definition val_ok (e:env) (i:val) :=
∀ n T, nth_error e n = value T -> el (lift (S n) T) i (i n).
Lemma vcons_add_var0 : ∀ e T i x,
val_ok e i -> el T i x -> val_ok (T::e) (V.cons x i).
Lemma vcons_add_var : ∀ e T i x,
val_ok e i -> x ∈ int T i -> val_ok (T::e) (V.cons x i).
Lemma add_var_eq_fun : ∀ T U U' i,
(∀ x, el T i x -> int U (V.cons x i) == int U' (V.cons x i)) ->
eq_fun (int T i)
(fun x => int U (V.cons x i))
(fun x => int U' (V.cons x i)).
Typing
Equality
Subtyping
Alternative equality (with kind=kind)
Definition eq_typ' e M M' :=
eq_typ e M M' /\ match M,M' with None,None => True|Some _,Some _=>True|_,_=>False end.
eq_typ e M M' /\ match M,M' with None,None => True|Some _,Some _=>True|_,_=>False end.
Subtyping as inclusion of values
Definition sub_typ' (e:env) (M M':term) :=
∀ i x, val_ok e i -> el M i x -> el M' i x.
Global Instance typ_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (typ e).
Qed.
Global Instance eq_typ_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (eq_typ e).
Qed.
Global Instance sub_typ_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (sub_typ e).
Qed.
Global Instance sub_typ'_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (sub_typ' e).
Qed.
End J.
Import J.
∀ i x, val_ok e i -> el M i x -> el M' i x.
Global Instance typ_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (typ e).
Qed.
Global Instance eq_typ_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (eq_typ e).
Qed.
Global Instance sub_typ_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (sub_typ e).
Qed.
Global Instance sub_typ'_morph : ∀ e, Proper (eq_term ==> eq_term ==> iff) (sub_typ' e).
Qed.
End J.
Import J.
Equality rules
Lemma refl : ∀ e M, eq_typ e M M.
Lemma sym : ∀ e M M', eq_typ e M M' -> eq_typ e M' M.
Lemma trans : ∀ e M M' M'', eq_typ e M M' -> eq_typ e M' M'' -> eq_typ e M M''.
Global Instance eq_typ_equiv : ∀ e, Equivalence (eq_typ e).
Qed.
Lemma eq_typ_app : ∀ e M M' N N',
eq_typ e M M' ->
eq_typ e N N' ->
eq_typ e (App M N) (App M' N').
Lemma eq_typ_abs : ∀ e T T' M M',
eq_typ e T T' ->
eq_typ (T::e) M M' ->
eq_typ e (Abs T M) (Abs T' M').
Lemma eq_typ_prod : ∀ e T T' U U',
eq_typ e T T' ->
eq_typ (T::e) U U' ->
eq_typ e (Prod T U) (Prod T' U').
Lemma eq_typ_beta : ∀ e T M M' N N',
eq_typ (T::e) M M' ->
eq_typ e N N' ->
typ e N T ->
T <> kind ->
eq_typ e (App (Abs T M) N) (subst N' M').
Typing rules
Lemma typ_prop : ∀ e, typ e prop kind.
Lemma typ_var : ∀ e n T,
nth_error e n = value T -> typ e (Ref n) (lift (S n) T).
Lemma typ_app : ∀ e u v V Ur,
typ e v V ->
typ e u (Prod V Ur) ->
V <> kind ->
typ e (App u v) (subst v Ur).
Lemma typ_abs : ∀ e T M U,
typ (T :: e) M U ->
U <> kind ->
typ e (Abs T M) (Prod T U).
Lemma typ_beta : ∀ e T M N U,
typ e N T ->
typ (T::e) M U ->
T <> kind ->
U <> kind ->
typ e (App (Abs T M) N) (subst N U).
Lemma typ_prod : ∀ e T U s2,
s2 = kind \/ s2 = prop ->
typ (T :: e) U s2 ->
typ e (Prod T U) s2.
Lemma typ_conv : ∀ e M T T',
typ e M T ->
eq_typ e T T' ->
T <> kind ->
typ e M T'.
Weakening
Lemma weakening : ∀ e M T A,
typ e M T ->
typ (A::e) (lift 1 M) (lift 1 T).
Lemma weakening0 : ∀ e M T,
typ e M T ->
typ e (lift 0 M) (lift 0 T).
Lemma weakeningS : ∀ e k M T A,
typ e (lift k M) (lift k T) ->
typ (A::e) (lift (S k) M) (lift (S k) T).
Subtyping
Lemma sub_refl : ∀ e M M',
eq_typ e M M' -> sub_typ e M M'.
Lemma sub_trans : ∀ e M1 M2 M3,
sub_typ e M1 M2 -> sub_typ e M2 M3 -> sub_typ e M1 M3.
Lemma typ_subsumption : ∀ e M T T',
typ e M T ->
sub_typ e T T' ->
T <> kind ->
typ e M T'.
Lemma sub_refl' : ∀ e M M',
eq_typ' e M M' -> sub_typ' e M M'.
Lemma sub_trans' : ∀ e M1 M2 M3,
sub_typ' e M1 M2 -> sub_typ' e M2 M3 -> sub_typ' e M1 M3.
Lemma typ_subsumption' : ∀ e M T T',
typ e M T ->
sub_typ' e T T' ->
typ e M T'.
End R.
Hint Resolve in_int_el.
eq_typ e M M' -> sub_typ e M M'.
Lemma sub_trans : ∀ e M1 M2 M3,
sub_typ e M1 M2 -> sub_typ e M2 M3 -> sub_typ e M1 M3.
Lemma typ_subsumption : ∀ e M T T',
typ e M T ->
sub_typ e T T' ->
T <> kind ->
typ e M T'.
Lemma sub_refl' : ∀ e M M',
eq_typ' e M M' -> sub_typ' e M M'.
Lemma sub_trans' : ∀ e M1 M2 M3,
sub_typ' e M1 M2 -> sub_typ' e M2 M3 -> sub_typ' e M1 M3.
Lemma typ_subsumption' : ∀ e M T T',
typ e M T ->
sub_typ' e T T' ->
typ e M T'.
End R.
Hint Resolve in_int_el.
Consistency