cic-model/ModelHF.v at master · barras/cic-model · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135

(** A finitary model of the calculus of construction: hereditarily
    finite sets.
 *)

Require Import Bool List.
Require Import HFcoc.
Require Import Models GenModelSyntax.

(** * Instance of the abstract model *)

Module HF_Coc_Model <: CC_Model.

Definition X := hf.
Definition inX := In_hf.
Definition eqX := Eq_hf.
Definition eqX_equiv : Equivalence Eq_hf.
split.
 apply eq_hf_refl.
 apply eq_hf_sym.
 apply eq_hf_trans.
Qed.
Definition inclX := Incl_hf.

Notation "x ∈ y" := (inX x y).
Notation "x == y" := (eqX x y).

Lemma in_ext: Proper (eqX ==> eqX ==> iff) inX.
Proof In_hf_morph.

Definition props := props.
Definition app := cc_app.
Definition lam := cc_lam.
Definition prod := cc_prod.

Definition eq_fun (x:X) (f1 f2:X->X) :=
  forall y1 y2, y1 ∈ x -> y1 == y2 -> f1 y1 == f2 y2.

Lemma lam_ext :
  forall x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  lam x1 f1 == lam x2 f2.
Proof cc_lam_ext.

Lemma app_ext: Proper (eqX ==> eqX ==> eqX) app.
Proof cc_app_morph.

Lemma prod_ext :
  forall x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  prod x1 f1 == prod x2 f2.
Proof cc_prod_ext.

Lemma prod_intro : forall dom f F,
  eq_fun dom f f ->
  eq_fun dom F F ->
  (forall x, x ∈ dom -> f x ∈ F x) ->
  lam dom f ∈ prod dom F.
Proof cc_prod_intro.

Lemma prod_elim : forall dom f x F,
  eq_fun dom F F ->
  f ∈ prod dom F ->
  x ∈ dom ->
  app f x ∈ F x.
Proof cc_prod_elim.

Lemma impredicative_prod : forall dom F,
  eq_fun dom F F ->
  (forall x, x ∈ dom -> F x ∈ props) ->
  prod dom F ∈ props.
Proof cc_impredicative_prod.

Lemma beta_eq:
  forall dom F x,
  eq_fun dom F F ->
  x ∈ dom ->
  app (lam dom F) x == F x.
Proof cc_beta_eq.

End HF_Coc_Model.

Module Soundness := GenModelSyntax.MakeModel(HF_Coc_Model).

Import Soundness.
Import T.

(** * Principles supported by the model *)

(** Deciding whether [f] is true for all valuations *)
Fixpoint forall_int_env (e:Env.env) (f:(nat->hf)->bool) {struct e} : bool :=
  match e with
    nil => f (fun _ => empty)
  | T::e' => forall_int_env e'
      (fun i_f => forall_elt (fun x => f (V.cons x i_f)) (int (int_trm T) i_f))
  end.

(** Deciding whether a context is satisfiable *)
Definition valid_context (e:Env.env) : bool :=
  negb (forall_int_env e (fun _ => false)).

(*
  Lemma valid_context_ok : forall e,
    valid_context e = true -> forall M M', ~ eq_typ e M M' FALSE.
*)

Require Import Term TypeJudge.

Definition int_clos T := int (int_trm T) vnil.

(** ** Consistency of CC *)
  Lemma cc_consistency : forall M M', ~ eq_typ nil M M' FALSE.
apply non_provability.
 intros.
 Time compute.
 discriminate.
Qed.


(** ** Properties not validated by the model *)
Eval vm_compute in (int_clos FALSE). (*consistency *)

(** ** Properties validated by the model *)
Eval vm_compute in (int_clos TRUE).

(** NAT is inhabited *)
Eval vm_compute in (int_clos INAT).
(** excluded-middle: *)
Eval vm_compute in (int_clos EM).
(** proof-irrelevance: *)
Eval vm_compute in (int_clos PI).
(** extensionality of funs of Prop -> Prop *)
Eval vm_compute in (int_clos (EXT prop prop)).