Models.v 17.9 KB
Newer Older
Pierre Letouzey's avatar
Pierre Letouzey committed
1
2
3
4
5
6

(** * Models of theories *)

(** The NatDed development, Pierre Letouzey, 2019.
    This file is released under the CC0 License, see the LICENSE file *)

7
Require Import Eqdep_dec Defs Mix NameProofs Meta ProofExamples.
8
Require Import Wellformed Theories NaryFunctions Nary PreModels.
Pierre Letouzey's avatar
Pierre Letouzey committed
9
10
11
12
13
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope eqb_scope.

14
15
16
17
18
19
20
21
(** We'll frequently consider interpretations of formulas over all
    possible global environments, so here's a convenient shortcut *)

Definition interp {sign M} (mo : PreModel M sign) A :=
  forall G, finterp mo G [] A.

(** A Model is a PreModel that satisfies all the axioms of the theory. *)

Pierre Letouzey's avatar
Pierre Letouzey committed
22
23
Record Model (M:Type)(th : theory) :=
 { pre :> PreModel M th;
24
   AxOk : forall A, IsAxiom th A -> interp pre A }.
Pierre Letouzey's avatar
Pierre Letouzey committed
25

Pierre Letouzey's avatar
Pierre Letouzey committed
26
Lemma validity_theorem logic th :
Pierre Letouzey's avatar
Pierre Letouzey committed
27
28
 CoqRequirements logic ->
 forall T, IsTheorem logic th T ->
29
 forall M (mo : Model M th), interp mo T.
Pierre Letouzey's avatar
Pierre Letouzey committed
30
Proof.
31
 intros CR T Thm M mo G.
Pierre Letouzey's avatar
Pierre Letouzey committed
32
 rewrite thm_alt in Thm.
33
 destruct Thm as (WF & d & axs & ((CK & BC) & V) & F & C).
34
 assert (CO:=@correctness th M mo logic d CR V BC G).
Pierre Letouzey's avatar
Pierre Letouzey committed
35
36
37
38
39
40
41
42
43
 rewrite C in CO. apply CO. intros A HA. apply AxOk.
 rewrite Forall_forall in F; auto.
Qed.

Lemma consistency_by_model logic th :
 CoqRequirements logic ->
 { M & Model M th } -> Consistent logic th.
Proof.
 intros CR (M,mo) Thm.
Pierre Letouzey's avatar
Pierre Letouzey committed
44
 apply (validity_theorem _ _ CR _ Thm M mo (fun _ => mo.(someone))).
Pierre Letouzey's avatar
Pierre Letouzey committed
45
46
Qed.

47
48
49
Record cterm sign :=
  { this :> term;
    closed : wc sign this = true }.
Pierre Letouzey's avatar
Pierre Letouzey committed
50

51
Arguments this {sign}.
Pierre Letouzey's avatar
Pierre Letouzey committed
52

53
54
Lemma proof_irr sign (s s' : cterm sign) :
 s = s' <-> s.(this) = s'.(this).
Pierre Letouzey's avatar
Pierre Letouzey committed
55
Proof.
56
 destruct s as (t,w), s' as (t',w'). cbn. split.
Pierre Letouzey's avatar
Pierre Letouzey committed
57
58
 - now injection 1.
 - intros <-. f_equal.
59
   destruct (wc sign t); [|easy].
Pierre Letouzey's avatar
Pierre Letouzey committed
60
61
   rewrite UIP_refl_bool. apply UIP_refl_bool.
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
62
63
64
65
66
67

Section SyntacticPreModel.
Variable th : theory.
Variable oneconst : string.
Hypothesis Honeconst : th.(funsymbs) oneconst = Some 0.

68
Let M := cterm th.
Pierre Letouzey's avatar
Pierre Letouzey committed
69

70
71
72
Definition oneM :=
  {| this := Cst oneconst;
     closed := Cst_wc _ _ Honeconst |}.
Pierre Letouzey's avatar
Pierre Letouzey committed
73

74
75
76
Lemma cons_ok n (t : cterm th) (v : term^n) :
 Forall (WC th) (nprod_to_list v) ->
 Forall (WC th) (nprod_to_list (n:=S n) (t.(this),v)).
Pierre Letouzey's avatar
Pierre Letouzey committed
77
Proof.
78
 intros W. cbn. constructor; auto. apply term_wc_iff, closed.
Pierre Letouzey's avatar
Pierre Letouzey committed
79
80
Qed.

81
82
(** [these] : convert to list + repeat the [this] projection to terms *)
Definition these {n} (v:M^n) := map this (nprod_to_list v).
Pierre Letouzey's avatar
Pierre Letouzey committed
83

84
85
86
Lemma closed_fun f n (v:M^n) :
 funsymbs th f = Some n ->
 wc th (Fun f (these v)) = true.
Pierre Letouzey's avatar
Pierre Letouzey committed
87
88
Proof.
 intros E.
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
 rewrite <- term_wc_iff, Fun_WC.
 unfold these. rewrite map_length, nprod_to_list_length.
 split; trivial.
 clear E.
 revert v.
 induction n; destruct v; cbn; constructor; auto.
 apply term_wc_iff, closed.
Qed.

(** Note : the decidability on [option nat] below is mainly to avoid
    some mess in dependent equality. It's morally always [left E]. *)
Definition syntactic_fun f n (v:M^n) : M :=
  match option_nat_dec (funsymbs th f) (Some n) with
  | left E => {| this := Fun f (these v); closed := closed_fun f n v E |}
  | right _ => oneM
  end.
Pierre Letouzey's avatar
Pierre Letouzey committed
105

106
107
108
109
110
111
112
113
Definition syntactic_pred p n (v:M^n) : Prop :=
  IsTheorem K th (Pred p (these v)).

Definition mkfuns f : optnfun M M :=
 match funsymbs th f with
 | Some n => NFun n (ncurry (syntactic_fun f n))
 | None => Nop
 end.
Pierre Letouzey's avatar
Pierre Letouzey committed
114

115
116
117
118
119
Definition mkpreds p : optnfun M Prop :=
 match predsymbs th p with
 | Some n => NFun n (ncurry (syntactic_pred p n))
 | None => Nop
 end.
Pierre Letouzey's avatar
Pierre Letouzey committed
120

121
Lemma mkfuns_ok f : funsymbs th f = get_arity (mkfuns f).
Pierre Letouzey's avatar
Pierre Letouzey committed
122
Proof.
123
 unfold mkfuns. now destruct (funsymbs th f).
Pierre Letouzey's avatar
Pierre Letouzey committed
124
125
Qed.

126
127
Lemma syntactic_fun_some f n (v:M^n) : funsymbs th f = Some n ->
 this (syntactic_fun f n v) = Fun f (these v).
Pierre Letouzey's avatar
Pierre Letouzey committed
128
Proof.
129
130
131
 unfold syntactic_fun. intros E.
 destruct option_nat_dec as [|[ ]]; auto.
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
132

133
Lemma mkpreds_ok p : predsymbs th p = get_arity (mkpreds p).
Pierre Letouzey's avatar
Pierre Letouzey committed
134
Proof.
135
 unfold mkpreds. now destruct predsymbs.
Pierre Letouzey's avatar
Pierre Letouzey committed
136
137
138
Qed.

Definition SyntacticPreModel : PreModel M th :=
139
140
141
142
143
 {| someone := oneM;
    funs := mkfuns;
    preds := mkpreds;
    funsOk := mkfuns_ok;
    predsOk := mkpreds_ok |}.
Pierre Letouzey's avatar
Pierre Letouzey committed
144
145
146
147
148

End SyntacticPreModel.

Section SyntacticModel.
Variable th : theory.
149
150
151
Hypothesis consistent : Consistent K th.
Hypothesis complete : Complete K th.
Hypothesis witsat : WitnessSaturated K th.
Pierre Letouzey's avatar
Pierre Letouzey committed
152
153
154
Variable oneconst : string.
Hypothesis Honeconst : th.(funsymbs) oneconst = Some 0.

155
156
157
158
159
Let M := cterm th.

Let mo : PreModel M th := SyntacticPreModel th oneconst Honeconst.

Implicit Types G : variable -> M.
160
161
Implicit Types t : term.
Implicit Types A : formula.
Pierre Letouzey's avatar
Pierre Letouzey committed
162

163
Definition closure {T}`{VMap T} G : T -> T := vmap G.
Pierre Letouzey's avatar
Pierre Letouzey committed
164

165
166
Lemma tclosure_check G t :
  check th (closure G t) = check th t.
Pierre Letouzey's avatar
Pierre Letouzey committed
167
Proof.
168
169
 induction t using term_ind'; cbn; auto.
 - destruct G as (t,Ht); cbn; auto. apply term_wc_iff in Ht. apply Ht.
Pierre Letouzey's avatar
Pierre Letouzey committed
170
171
172
 - rewrite map_length.
   destruct (funsymbs th f); [|easy].
   case eqb; [|easy].
173
   rewrite forallb_map. now apply forallb_ext.
Pierre Letouzey's avatar
Pierre Letouzey committed
174
175
Qed.

176
177
Lemma tclosure_level G t :
  level (closure G t) = level t.
Pierre Letouzey's avatar
Pierre Letouzey committed
178
Proof.
179
180
181
 induction t using term_ind'; cbn; auto.
 - destruct G as (t,Ht); cbn; auto. apply term_wc_iff in Ht. apply Ht.
 - rewrite map_map. now apply list_max_map_ext.
Pierre Letouzey's avatar
Pierre Letouzey committed
182
183
Qed.

184
Lemma tclosure_fclosed G t : FClosed (closure G t).
Pierre Letouzey's avatar
Pierre Letouzey committed
185
Proof.
186
 induction t using term_ind'; cbn; auto.
187
188
189
190
 - destruct G as (t,Ht); cbn; auto. apply term_wc_iff in Ht. apply Ht.
 - rewrite <- term_fclosed_spec. cbn.
   rewrite forallb_map.
   apply forallb_forall. now setoid_rewrite term_fclosed_spec.
Pierre Letouzey's avatar
Pierre Letouzey committed
191
192
Qed.

193
194
Lemma fclosure_check G A :
 check th (closure G A) = check th A.
Pierre Letouzey's avatar
Pierre Letouzey committed
195
Proof.
196
 induction A; cbn; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
197
198
199
 - rewrite map_length.
   destruct predsymbs; [|easy].
   case eqb; [|easy].
200
   rewrite forallb_map. apply forallb_ext. intros x _.
201
202
   apply tclosure_check.
 - now rewrite IHA1, IHA2.
Pierre Letouzey's avatar
Pierre Letouzey committed
203
204
Qed.

205
206
Lemma fclosure_level G A :
  level (closure G A) = level A.
Pierre Letouzey's avatar
Pierre Letouzey committed
207
Proof.
208
 induction A; cbn; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
209
 revert l. induction l as [|t l IH]; cbn; auto.
210
 f_equal; auto. apply tclosure_level.
Pierre Letouzey's avatar
Pierre Letouzey committed
211
212
Qed.

213
214
Lemma fclosure_fclosed G A :
  FClosed (closure G A).
Pierre Letouzey's avatar
Pierre Letouzey committed
215
Proof.
216
217
 induction A; cbn; auto.
 - change (FClosed (Pred p (map (closure G) l))).
218
   rewrite <- form_fclosed_spec. cbn.
219
220
   rewrite forallb_map.
   apply forallb_forall. intros x _. rewrite term_fclosed_spec.
221
   apply tclosure_fclosed.
222
 - rewrite <- form_fclosed_spec in *. cbn. now rewrite lazy_andb_iff.
Pierre Letouzey's avatar
Pierre Letouzey committed
223
224
Qed.

225
226
Lemma tclosure_wc G t:
  WF th t -> WC th (closure G t).
Pierre Letouzey's avatar
Pierre Letouzey committed
227
Proof.
228
 intros (?,?). repeat split.
229
230
231
 - now rewrite tclosure_check.
 - red. now rewrite tclosure_level.
 - apply tclosure_fclosed.
Pierre Letouzey's avatar
Pierre Letouzey committed
232
233
Qed.

234
235
Lemma tclosure_wc' G t :
  WF th t -> wc th (closure G t) = true.
Pierre Letouzey's avatar
Pierre Letouzey committed
236
Proof.
237
 intro. apply term_wc_iff. now apply tclosure_wc.
Pierre Letouzey's avatar
Pierre Letouzey committed
238
239
Qed.

240
241
Lemma fclosure_wc G A :
  WF th A -> WC th (closure G A).
Pierre Letouzey's avatar
Pierre Letouzey committed
242
Proof.
243
 intros (?,?). repeat split.
244
245
246
 - now rewrite fclosure_check.
 - red. now rewrite fclosure_level.
 - apply fclosure_fclosed.
Pierre Letouzey's avatar
Pierre Letouzey committed
247
248
Qed.

249
Lemma fclosure_bsubst G n t A :
Pierre Letouzey's avatar
Pierre Letouzey committed
250
 FClosed t ->
251
 closure G (bsubst n t A) = bsubst n t (closure G A).
Pierre Letouzey's avatar
Pierre Letouzey committed
252
253
254
255
256
257
258
Proof.
 unfold closure.
 intros FC.
 rewrite form_vmap_bsubst.
 f_equal.
 rewrite term_vmap_id; auto.
 intros v. red in FC. intuition.
259
 intros v. destruct G as (u,Hu); simpl.
260
 apply term_wc_iff in Hu. apply Hu.
Pierre Letouzey's avatar
Pierre Letouzey committed
261
262
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
263
Lemma interp_pred p l :
264
 WF th (Pred p l) ->
265
 forall G,
266
   finterp mo G [] (Pred p l) <->
267
   IsTheorem K th
268
     (Pred p (map (fun t => this (tinterp mo G [] t)) l)).
269
270
271
272
273
274
275
276
277
278
Proof.
 rewrite Pred_WF. intros (E,F) G.
 cbn. unfold mkpreds. rewrite E.
 set (n := length l) in *.
 unfold napply_dft, optnapply.
 destruct optnprod as [a|] eqn:E'.
 2:{ exfalso. revert E'. apply optnprod_some. now rewrite map_length. }
 cbn. rewrite nuncurry_ncurry. unfold syntactic_pred. f_equiv.
 f_equal. unfold these.
 apply optnprod_to_list in E'. fold M. now rewrite E', map_map.
Pierre Letouzey's avatar
Pierre Letouzey committed
279
280
Qed.

281
Lemma tinterp_carac t :
282
 WF th t ->
283
 forall G, this (tinterp mo G [] t) = closure G t.
Pierre Letouzey's avatar
Pierre Letouzey committed
284
285
Proof.
 induction t as [ | | f l IH] using term_ind'; cbn; auto.
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
 - now rewrite wf_iff.
 - rewrite Fun_WF. intros (E,F) G.
   set (n := length l) in *.
   unfold napply_dft, optnapply.
   unfold mkfuns. rewrite E.
   destruct optnprod as [a|] eqn:E'.
   2:{ exfalso. revert E'. apply optnprod_some. now rewrite map_length. }
   cbn.
   rewrite nuncurry_ncurry.
   rewrite syntactic_fun_some; auto.
   f_equal. unfold these.
   apply optnprod_to_list in E'. fold M. rewrite E', map_map.
   apply map_ext_iff. intros x Hx. apply IH; auto.
   revert x Hx. now apply Forall_forall.
Qed.

302
303
Lemma tinterp_carac' (t:term) G (W : WF th t) :
  tinterp mo G [] t =
304
  {| this := closure G t; closed := tclosure_wc' G t W |}.
Pierre Letouzey's avatar
Pierre Letouzey committed
305
Proof.
306
 apply proof_irr. cbn. now apply tinterp_carac.
Pierre Letouzey's avatar
Pierre Letouzey committed
307
308
Qed.

309
310
311
(** For a consistent and complete theory, [IsTheorem] has some nice
    extra properties : *)

312
313
Lemma Thm_Not A : WC th A ->
 IsTheorem K th (~A) <-> ~IsTheorem K th A.
Pierre Letouzey's avatar
Pierre Letouzey committed
314
315
316
317
318
319
320
Proof.
 split.
 - intros Thm' Thm. apply consistent.
   apply Thm_Not_e with A; auto.
 - destruct (complete A); trivial. now intros [ ].
Qed.

321
Lemma Thm_Or A B : WC th (A\/B) ->
322
323
  IsTheorem K th A \/ IsTheorem K th B <->
  IsTheorem K th (A \/ B).
Pierre Letouzey's avatar
Pierre Letouzey committed
324
325
326
Proof.
 intros WF.
 split.
327
328
 - now apply Thm_or_i.
 - intros (_ & axs & F & Por); rewrite Op_WC in WF.
Pierre Letouzey's avatar
Pierre Letouzey committed
329
   destruct (complete A) as [HA|HA]; [easy|now left|].
330
   destruct HA as (_ & axsA & FA & PnA).
Pierre Letouzey's avatar
Pierre Letouzey committed
331
   destruct (complete B) as [HB|HB]; [easy|now right|].
332
   destruct HB as (_ & axsB & FB & PnB).
Pierre Letouzey's avatar
Pierre Letouzey committed
333
   destruct consistent.
334
335
   split. apply False_WC.
   exists (axs++axsA++axsB). split; [now rewrite !Forall_app|].
Pierre Letouzey's avatar
Pierre Letouzey committed
336
   apply R_Or_e with A B.
337
338
339
340
341
   + now apply Pr_app_l.
   + eapply R_Not_e; [apply R'_Ax|].
     now apply Pr_pop, Pr_app_r, Pr_app_l.
   + eapply R_Not_e; [apply R'_Ax|].
     now apply Pr_pop, Pr_app_r, Pr_app_r.
Pierre Letouzey's avatar
Pierre Letouzey committed
342
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
343

344
Lemma Thm_Imp A B : WC th (A->B) ->
345
346
  (IsTheorem K th A -> IsTheorem K th B) <->
  IsTheorem K th (A -> B).
Pierre Letouzey's avatar
Pierre Letouzey committed
347
Proof.
348
349
350
351
352
353
354
355
356
357
358
 intros W. split; try apply Thm_Imp_e.
 intros IM.
 destruct (complete A) as [HA|HA]; [rewrite Op_WC in W; easy | | ].
 - destruct (IM HA) as (_ & axs & F & P). split; auto.
   exists axs; split; auto.
   apply R_Imp_i. now apply Pr_pop.
 - destruct HA as (_ & axs & F & P). split; auto.
   exists axs; split; auto.
   apply R_Imp_i.
   apply R_Fa_e.
   eapply R_Not_e; [apply R'_Ax|]. now apply Pr_pop.
Pierre Letouzey's avatar
Pierre Letouzey committed
359
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
360
361


Pierre Letouzey's avatar
Pierre Letouzey committed
362
363
364
365
366
367
368
369
Fixpoint height f :=
  match f with
  | True | False | Pred _ _ => 0
  | Not f => S (height f)
  | Op _ f1 f2 => S (Nat.max (height f1) (height f2))
  | Quant _ f => S (height f)
  end.

Pierre Letouzey's avatar
Pierre Letouzey committed
370
371
372
Lemma height_bsubst n t f :
 height (bsubst n t f) = height f.
Proof.
373
 revert n t.
Pierre Letouzey's avatar
Pierre Letouzey committed
374
375
376
 induction f; cbn; f_equal; auto.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
377
378
379
380
381
382
383
384
385
386
387
388
Lemma height_ind (P : formula -> Prop) :
 (forall h, (forall f, height f < h -> P f) ->
            (forall f, height f < S h -> P f)) ->
 forall f, P f.
Proof.
 intros IH f.
 set (h := S (height f)).
 assert (LT : height f < h) by (cbn; auto with * ).
 clearbody h. revert f LT.
 induction h as [|h IHh]; [inversion 1|eauto].
Qed.

389
390
Lemma interp_carac A : WF th A ->
 forall G, finterp mo G [] A <-> IsTheorem K th (closure G A).
Pierre Letouzey's avatar
Pierre Letouzey committed
391
Proof.
392
393
 induction A as [h IH A HA] using height_ind. destruct A; intros W G.
 - clear IH HA. cbn.
Pierre Letouzey's avatar
Pierre Letouzey committed
394
395
   unfold IsTheorem. intuition.
   now exists [].
396
 - clear IH HA. cbn.
Pierre Letouzey's avatar
Pierre Letouzey committed
397
   unfold IsTheorem. intuition.
Pierre Letouzey's avatar
Pierre Letouzey committed
398
   apply consistent; split; auto.
399
400
401
 - clear IH HA.
   rewrite interp_pred; auto. f_equiv. cbn. f_equiv.
   apply map_ext_iff. intros t Ht.
402
   apply tinterp_carac. revert t Ht. apply Forall_forall.
403
   now apply Pred_WF in W.
Pierre Letouzey's avatar
Pierre Letouzey committed
404
 - simpl. rewrite IH; auto with arith.
405
   symmetry. apply Thm_Not.
406
407
   apply fclosure_wc; auto.
 - assert (W' := fclosure_wc G _ W).
408
   apply Op_WF in W.
409
   cbn in HA. apply Nat.succ_lt_mono in HA. apply max_lt in HA.
410
411
   destruct o; simpl; rewrite !IH by easy.
   + apply Thm_And.
412
413
   + now apply Thm_Or.
   + now apply Thm_Imp.
Pierre Letouzey's avatar
Pierre Letouzey committed
414
 - simpl.
415
416
   cbn in HA. apply Nat.succ_lt_mono in HA.
   assert (L : level A <= 1).
417
   { unfold WF,BClosed in W. cbn in W. omega. }
418
   assert (HA' : forall t, height (bsubst 0 t A) < h).
419
   { intro. now rewrite height_bsubst. }
Pierre Letouzey's avatar
Pierre Letouzey committed
420
421
   destruct q; split.
   + intros H.
422
423
424
425
426
     destruct (complete (closure G (~A)%form));
      [apply fclosure_wc; auto| | ].
     * destruct (witsat (closure G (~A)%form) H0) as (c & Hc & Thm).
       rewrite <- fclosure_bsubst in Thm by auto.
       change (closure _ _) with (~closure G (bsubst 0 (Cst c) A))%form
427
        in Thm.
428
       assert (WF th (bsubst 0 (Cst c) A)).
429
430
431
432
       { split.
         - apply check_bsubst; cbn; auto. now rewrite Hc, eqb_refl.
           apply W.
         - apply Nat.le_0_r, level_bsubst; auto. }
433
       rewrite Thm_Not in Thm by (apply fclosure_wc; auto).
Pierre Letouzey's avatar
Pierre Letouzey committed
434
       rewrite <- IH in Thm; auto.
435
       rewrite <- finterp_bsubst0 in Thm; auto. destruct Thm. apply H.
436
     * cbn. apply Thm_NotExNot; auto. apply (fclosure_wc _ (A)); auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
437
   + intros Thm (t,Ht).
438
     rewrite finterp_bsubst0 with (u:=t); auto.
439
440
     2:{ apply term_wc_iff in Ht. apply Ht. }
     2:{ destruct (proj2 (term_wc_iff _ _) Ht) as (W',F').
441
         rewrite (tinterp_carac' t G W').
Pierre Letouzey's avatar
Pierre Letouzey committed
442
         apply proof_irr. cbn. apply term_vmap_id. intros v.
443
444
445
         red in F'. intuition. }
     apply term_wc_iff in Ht.
     rewrite IH; auto.
446
     * rewrite fclosure_bsubst by apply Ht. apply Thm_All_e; auto.
447
     * apply bsubst_WF; auto. apply Ht.
Pierre Letouzey's avatar
Pierre Letouzey committed
448
   + intros ((t,Ht),Int).
449
     rewrite finterp_bsubst0 with (u:=t) in Int; auto.
450
     2:{ clear Int. apply term_wc_iff in Ht. apply Ht. }
Pierre Letouzey's avatar
Pierre Letouzey committed
451
     2:{ clear Int.
452
         destruct (proj2 (term_wc_iff _ _) Ht) as (W',F').
453
         rewrite (tinterp_carac' t G W').
Pierre Letouzey's avatar
Pierre Letouzey committed
454
         apply proof_irr. cbn. apply term_vmap_id. intros v.
455
456
457
         red in F'. intuition. }
     apply term_wc_iff in Ht.
     rewrite IH in Int; auto.
458
     * rewrite fclosure_bsubst in Int by apply Ht.
459
       apply Thm_Ex_i with t; auto.
460
       apply (fclosure_wc _ (A)); auto.
461
     * apply bsubst_WF; auto. apply Ht.
Pierre Letouzey's avatar
Pierre Letouzey committed
462
   + intros Thm.
463
464
     destruct (witsat (closure G A) Thm) as (c & Hc & Thm').
     rewrite <- fclosure_bsubst in Thm' by auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
465
     rewrite <- IH in Thm'.
466
467
     2:{ now rewrite height_bsubst. }
     2:{ apply bsubst_WF; auto. now apply Cst_WC. }
468
     exists {| this := Cst c; closed := Cst_wc th c Hc |}.
469
470
     rewrite finterp_bsubst0; eauto.
     apply proof_irr. rewrite tinterp_carac; auto. now apply Cst_WC.
Pierre Letouzey's avatar
Pierre Letouzey committed
471
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
472

473
474
Lemma interp_carac_closed G A : WC th A ->
 finterp mo G [] A <-> IsTheorem K th A.
Pierre Letouzey's avatar
Pierre Letouzey committed
475
Proof.
476
 intros W.
477
 replace A with (closure G A) at 2.
478
479
480
 apply interp_carac. apply W.
 apply form_vmap_id. intros v. destruct W as (_,F).
 red in F. intuition.
Pierre Letouzey's avatar
Pierre Letouzey committed
481
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
482

483
Lemma axioms_ok A : IsAxiom th A -> interp mo A.
Pierre Letouzey's avatar
Pierre Letouzey committed
484
Proof.
485
 intros HA G. apply interp_carac_closed.
486
 apply WCAxiom; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
487
488
489
490
491
492
493
494
495
 apply ax_thm; auto.
Qed.

Definition SyntacticModel : Model M th :=
 {| pre := mo;
    AxOk := axioms_ok |}.

End SyntacticModel.

496
497
498
Definition nopify {X Y} (o:option nat) (f:optnfun X Y) :=
  match o with None => Nop | _ => f end.

Pierre Letouzey's avatar
Pierre Letouzey committed
499
500
501
502
Lemma premodel_restrict sign sign' M :
 SignExtend sign sign' ->
 PreModel M sign' -> PreModel M sign.
Proof.
503
504
505
 intros SE mo'.
 set (fs := fun f => nopify (funsymbs sign f) (funs mo' f)).
 set (ps := fun f => nopify (predsymbs sign f) (preds mo' f)).
Pierre Letouzey's avatar
Pierre Letouzey committed
506
 apply Build_PreModel with fs ps.
507
 - exact mo'.(someone).
Pierre Letouzey's avatar
Pierre Letouzey committed
508
 - intros f. unfold fs.
509
510
   generalize (funsOk mo' f).
   destruct SE as (SE,_). destruct (SE f) as [-> | ->]; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
511
512
   destruct (funsymbs sign' f); auto.
 - intros p. unfold ps.
513
514
   generalize (predsOk mo' p).
   destruct SE as (_,SE). destruct (SE p) as [-> | ->]; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
515
516
517
   destruct (predsymbs sign' p); auto.
Defined.

518
519
520
521
522
523
524
Lemma premodel_restrict_antiextend sign sign' M
 (E:SignExtend sign sign')(mo' : PreModel M sign') :
 PreModelExtend (premodel_restrict sign sign' M E mo') mo'.
Proof.
 repeat split; intros; unfold premodel_restrict; cbn.
 destruct funsymbs; red; auto.
 destruct predsymbs; red; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
525
526
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
527
Lemma model_restrict logic th th' M :
Pierre Letouzey's avatar
Pierre Letouzey committed
528
 CoqRequirements logic ->
Pierre Letouzey's avatar
Pierre Letouzey committed
529
530
 Extend logic th th' -> Model M th' -> Model M th.
Proof.
531
532
533
534
535
536
537
538
 intros CR (SE,EX) mo'.
 apply Build_Model with (premodel_restrict th th' M SE mo').
 intros A HA G.
 rewrite finterp_premodelext with (mo':=mo').
 - assert (Thm : IsTheorem logic th' A). { apply EX, ax_thm; auto. }
   eapply validity_theorem; eauto.
 - auto using premodel_restrict_antiextend.
 - now apply WCAxiom.
Pierre Letouzey's avatar
Pierre Letouzey committed
539
Defined.
Pierre Letouzey's avatar
Pierre Letouzey committed
540

Pierre Letouzey's avatar
Pierre Letouzey committed
541
Lemma consistent_has_model (th:theory) (nc : NewCsts th) :
Pierre Letouzey's avatar
Pierre Letouzey committed
542
 (forall A, A\/~A) ->
543
 Consistent K th ->
Pierre Letouzey's avatar
Pierre Letouzey committed
544
545
546
 { M & Model M th }.
Proof.
 intros EM C.
547
548
549
 set (th' := supercomplete K th nc).
 exists (cterm th').
 apply (model_restrict K th th'). red; intros; apply EM.
Pierre Letouzey's avatar
Pierre Letouzey committed
550
551
552
 apply supercomplete_extend.
 apply SyntacticModel with (oneconst := nc 0).
 - apply supercomplete_consistent; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
553
 - apply supercomplete_complete; auto. red; intros; apply EM.
Pierre Letouzey's avatar
Pierre Letouzey committed
554
555
556
557
558
559
560
561
562
 - apply supercomplete_saturated; auto.
 - unfold th'. cbn.
   replace (test th nc (nc 0)) with true; auto.
   symmetry. apply test_ok. now exists 0.
Qed.

Lemma completeness_theorem (th:theory) (nc : NewCsts th) :
 (forall A, A\/~A) ->
 forall T,
563
   WC th T ->
564
   (forall M (mo : Model M th) G, finterp mo G [] T)
565
   -> IsTheorem K th T.
Pierre Letouzey's avatar
Pierre Letouzey committed
566
567
Proof.
 intros EM T WF HT.
568
 destruct (EM (IsTheorem K th T)) as [Thm|NT]; auto.
569
 exfalso.
570
571
 assert (WC' : forall A, A = (~T)%form \/ IsAxiom th A -> WC th A).
 { intros A [->|HA]; auto using WCAxiom. }
572
573
 set (th' := {| sign := th;
                IsAxiom := fun f => f = (~T)%form \/ IsAxiom th f;
574
                WCAxiom := WC' |}).
575
576
577
578
579
580
 assert (nc' : NewCsts th').
 { apply (Build_NewCsts th')
   with (csts:=csts _ nc) (test:=test _ nc).
   - apply csts_inj.
   - intros. cbn. apply csts_ok.
   - apply test_ok. }
581
 assert (C : Consistent K th').
582
583
584
585
586
587
588
589
590
591
592
593
 { intros (_ & axs & F & P).
   set (axs' := filter (fun f => negb (f =? (~T)%form)) axs).
   apply NT; split; auto.
   exists axs'. split.
   - rewrite Forall_forall in *. intros A.
     unfold axs'. rewrite filter_In, negb_true_iff, eqb_neq.
     intros (HA,NE). destruct (F A HA); intuition.
   - apply R_Absu; auto.
     eapply Pr_weakening; eauto. constructor.
     intros A; simpl. unfold axs'.
     rewrite filter_In, negb_true_iff, eqb_neq.
     case (eqbspec A (~T)%form); intuition. }
594
 destruct (consistent_has_model th' nc' EM) as (M,mo'); auto.
595
 assert (EX : Extend K th th').
596
597
598
 { apply extend_alt. split.
   - cbn. apply signext_refl.
   - intros B HB. apply ax_thm. cbn. now right. }
599
600
601
 set (mo := model_restrict K th th' M EM EX mo').
 set (G := fun (_:variable) => mo'.(someone)).
 assert (finterp mo' G [] (~T)). { apply AxOk. cbn. now left. }
602
 cbn in H. apply H. clear H.
603
604
 rewrite <- finterp_premodelext with (mo:=mo); [apply HT| |apply WF].
 destruct EX. apply premodel_restrict_antiextend.
605
Qed.
606
607
608
609

(*
Print Assumptions completeness_theorem.
*)