Models.v 27.2 KB
Newer Older
Pierre Letouzey's avatar
Pierre Letouzey committed
1
2
Require Import Defs Mix Proofs Meta Omega Setoid Morphisms
  Eqdep_dec Theories PreModels.
Pierre Letouzey's avatar
Pierre Letouzey committed
3
4
5
6
7
8
9
10
11
12
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope eqb_scope.

Record Model (M:Type)(th : theory) :=
 { pre :> PreModel M th;
   AxOk : forall A, IsAxiom th A ->
                    forall genv, interp_form pre genv [] A }.

Pierre Letouzey's avatar
Pierre Letouzey committed
13
Lemma validity_theorem logic th :
Pierre Letouzey's avatar
Pierre Letouzey committed
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
 CoqRequirements logic ->
 forall T, IsTheorem logic th T ->
 forall M (mo : Model M th) genv, interp_form mo genv [] T.
Proof.
 intros CR T Thm M mo genv.
 rewrite thm_alt in Thm.
 destruct Thm as (WF & d & axs & (CK & BC & V) & F & C).
 assert (CO:=@correctness th M mo logic d CR V BC genv).
 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
31
 apply (validity_theorem _ _ CR _ Thm M mo (fun _ => mo.(someone))).
Pierre Letouzey's avatar
Pierre Letouzey committed
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
Qed.

Lemma Thm_Not_e th A :
 IsTheorem Classic th A -> IsTheorem Classic th (~A) ->
 IsTheorem Classic th False.
Proof.
 intros (_ & axs & F & PR) (_ & axs' & F' & PR').
 split. apply False_wf.
 exists (axs++axs'); split.
 rewrite Forall_forall in *; intros x; rewrite in_app_iff;
  intros [ | ]; auto.
 apply R_Not_e with A.
 - clear PR'; eapply Pr_weakening; eauto. constructor.
   intros a. rewrite in_app_iff; auto.
 - eapply Pr_weakening; eauto. constructor.
   intros a. rewrite in_app_iff; auto.
Qed.

Definition Wf_term (sign:signature) (t:term) :=
  check sign t = true /\ BClosed t /\ FClosed t.

Pierre Letouzey's avatar
Pierre Letouzey committed
53
54
55
56
57
58
59
60
61
62
63
64
65
Definition wf_term (sign:signature) (t:term) :=
 check sign t && (level t =? 0) && Vars.is_empty (fvars t).

Lemma Wf_term_alt sign t : Wf_term sign t <-> wf_term sign t = true.
Proof.
 unfold Wf_term, wf_term.
 split.
 - intros (-> & -> & H). cbn. now rewrite Vars.is_empty_spec.
 - rewrite !andb_true_iff, !eqb_eq. unfold BClosed.
   intros ((->,->),H); repeat split; auto.
   now rewrite Vars.is_empty_spec in H.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
66
Definition closed_term sign :=
Pierre Letouzey's avatar
Pierre Letouzey committed
67
68
69
70
71
72
73
74
75
76
77
 { t : term | wf_term sign t = true }.

Lemma proof_irr sign (s s' : closed_term sign) :
 s = s' <-> proj1_sig s = proj1_sig s'.
Proof.
 destruct s, s'. cbn. split.
 - now injection 1.
 - intros <-. f_equal.
   destruct (wf_term sign x); [|easy].
   rewrite UIP_refl_bool. apply UIP_refl_bool.
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
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

Fixpoint map_arity {A B B'}(f:B->B') n
 : arity_fun A n B -> arity_fun A n B' :=
 match n with
 | 0 => f
 | S n => fun ab a => map_arity f n (ab a)
 end.

Lemma build_map_arity {A B B'} n (l : list A)(f:B->B')(any:B)(any':B') :
 length l = n ->
 forall (a : arity_fun A n B),
 build_args n l any' (map_arity f n a) =
 f (build_args n l any a).
Proof.
 intros <-. induction l; simpl; auto.
Qed.


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

Let M := closed_term th.

Lemma cons_ok (t : term) (l : list term) n :
Pierre Letouzey's avatar
Pierre Letouzey committed
105
 wf_term th t = true ->
Pierre Letouzey's avatar
Pierre Letouzey committed
106
107
108
109
 length l = n /\ Forall (Wf_term th) l ->
 length (t::l) = S n /\ Forall (Wf_term th) (t::l).
Proof.
 intros WF (L,F).
Pierre Letouzey's avatar
Pierre Letouzey committed
110
 apply Wf_term_alt in WF.
Pierre Letouzey's avatar
Pierre Letouzey committed
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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
 split; simpl; auto.
Qed.

Definition sized_wf_listterm n :=
  {l : list term | length l = n /\ Forall (Wf_term th) l}.

Fixpoint mk_args n : arity_fun M n (sized_wf_listterm n) :=
 match n with
 | 0 => exist _ [] (conj eq_refl (Forall_nil _))
 | S n => fun t =>
          map_arity (fun '(exist _ l Hl) =>
                       let '(exist _ t Ht) := t in
                       exist _ (t::l) (cons_ok t l n Ht Hl))
                    n (mk_args n)
 end.

Lemma Fun_wf f l :
  Wf_term th (Fun f l) <->
   th.(funsymbs) f = Some (length l) /\ Forall (Wf_term th) l.
Proof.
 split.
 - intros (CK & BC & FC); cbn in *.
   destruct (funsymbs th f); [|easy].
   rewrite lazy_andb_iff, eqb_eq in CK.
   destruct CK as (->,CK). split; auto.
   rewrite forallb_forall in CK.
   apply Forall_forall. intros t Ht.
   repeat split; auto.
   + unfold BClosed in *. cbn in BC.
     rewrite list_max_map_0 in BC; auto.
   + unfold FClosed in *. cbn in FC.
     intros v. specialize (FC v). contradict FC.
     rewrite vars_unionmap_in. now exists t.
 - intros (E,F).
   rewrite Forall_forall in F.
   repeat split; cbn.
   + rewrite E, eqb_refl. apply forallb_forall.
     intros u Hu. now apply F.
   + red; cbn. apply list_max_map_0. intros u Hu. now apply F.
   + red; cbn. intro v. rewrite vars_unionmap_in.
     intros (a & IN & IN'). apply F in IN'. now apply IN' in IN.
Qed.

Lemma Pred_wf p l :
  Wf th (Pred p l) <->
   th.(predsymbs) p = Some (length l) /\ Forall (Wf_term th) l.
Proof.
 split.
 - intros (CK & BC & FC); cbn in *.
   destruct (predsymbs th p); [|easy].
   rewrite lazy_andb_iff, eqb_eq in CK.
   destruct CK as (->,CK). split; auto.
   rewrite forallb_forall in CK.
   apply Forall_forall. intros t Ht.
   repeat split; auto.
   + unfold BClosed in *. cbn in BC.
     rewrite list_max_map_0 in BC; auto.
   + unfold FClosed in *. cbn in FC.
     intros v. specialize (FC v). contradict FC.
     rewrite vars_unionmap_in. now exists t.
 - intros (E,F).
   rewrite Forall_forall in F.
   repeat split; cbn.
   + rewrite E, eqb_refl. apply forallb_forall.
     intros u Hu. now apply F.
   + red; cbn. apply list_max_map_0. intros u Hu. now apply F.
   + red; cbn. intro v. rewrite vars_unionmap_in.
     intros (a & IN & IN'). apply F in IN'. now apply IN' in IN.
Qed.

Lemma Cst_wf c :
  th.(funsymbs) c = Some 0 -> Wf_term th (Cst c).
Proof.
 intros. now apply Fun_wf.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
187
188
189
190
191
192
Lemma Cst_wf' c :
  th.(funsymbs) c = Some 0 -> wf_term th (Cst c) = true.
Proof.
 intros. now apply Wf_term_alt, Fun_wf.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
Definition one_listterm n : sized_wf_listterm n.
Proof.
 induction n as [|n (l & L & F)].
 - now exists [].
 - exists (Cst oneconst :: l).
   split; simpl; auto using Cst_wf.
Qed.

Lemma build_mk n (l : list M) (any:sized_wf_listterm n) :
 length l = n ->
 proj1_sig (build_args n l any (mk_args n)) =
 map (@proj1_sig _ _) l.
Proof.
 intros <-.
 induction l as [|(t,Ht) l IH]; simpl; auto.
 set (l0 := one_listterm (length l)).
 rewrite build_map_arity  with (any0:=l0); auto.
 specialize (IH l0).
 destruct (build_args _); simpl in *. f_equal; auto.
Qed.

Definition fun_core f n :
  (th.(funsymbs) f = Some n) -> arity_fun M n M.
Proof.
 intros E.
 generalize (mk_args n).
 apply map_arity. intros (l & Hl).
Pierre Letouzey's avatar
Pierre Letouzey committed
220
 exists (Fun f l). apply Wf_term_alt, Fun_wf; destruct Hl; subst; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
Defined.

Definition rich_funs f :
  { o : option { n:nat & arity_fun M n M } |
    th.(funsymbs) f = get_arity o /\
    match o with
    | None => Logic.True
    | Some (existT _ n a) =>
      forall (l: list M)(any : M), length l = n ->
        proj1_sig (build_args n l any a) =
        Fun f (map (@proj1_sig _ _) l)
    end }.
Proof.
 destruct (th.(funsymbs) f) as [n|] eqn:E.
 - set (r := fun_core f n E).
   exists (Some (existT _ n r)); split; auto.
   intros l any Hl.
   unfold r, fun_core.
   rewrite build_map_arity with (any0 := one_listterm n); auto.
   rewrite <- (build_mk n l (one_listterm n) Hl).
   destruct build_args. now cbn.
 - now exists None.
Defined.

Definition mk_funs : modfuns M :=
  fun f => proj1_sig (rich_funs f).

Lemma mk_funs_ok f : th.(funsymbs) f = get_arity (mk_funs f).
Proof.
 unfold mk_funs. now destruct (rich_funs f).
Qed.

Definition mk_preds : modpreds M.
Proof.
 intro p.
 destruct (th.(predsymbs) p) as [n|].
 - apply Some. exists n.
   generalize (mk_args n).
   apply map_arity.
   exact (fun sl => IsTheorem logic th (Pred p (proj1_sig sl))).
 - apply None.
Defined.

Lemma mk_preds_ok p : th.(predsymbs) p = get_arity (mk_preds p).
Proof.
 unfold mk_preds.
 now destruct (th.(predsymbs) p) as [n|].
Qed.

Definition SyntacticPreModel : PreModel M th :=
Pierre Letouzey's avatar
Pierre Letouzey committed
271
 {| someone := exist _ (Cst oneconst) (Cst_wf' _ Honeconst);
Pierre Letouzey's avatar
Pierre Letouzey committed
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
    funs := mk_funs;
    preds := mk_preds;
    funsOk := mk_funs_ok;
    predsOk := mk_preds_ok |}.

End SyntacticPreModel.

Section SyntacticModel.
Variable th : theory.
Hypothesis consistent : Consistent Classic th.
Hypothesis complete : Complete Classic th.
Hypothesis witsat : WitnessSaturated Classic th.
Variable oneconst : string.
Hypothesis Honeconst : th.(funsymbs) oneconst = Some 0.

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

Let term_closure (genv:variable -> M) (t:term) :=
  vmap (fun v:variable => proj1_sig (genv v)) t.

Let closure (genv:variable -> M) (f:formula) :=
  vmap (fun v:variable => proj1_sig (genv v)) f.

Pierre Letouzey's avatar
Pierre Letouzey committed
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
Lemma term_closure_check t (genv:variable->M) :
  check th (term_closure genv t) = check th t.
Proof.
 revert t.
 fix IH 1. destruct t as [ | | f l]; cbn; auto.
 - destruct (genv v) as (t,Ht); cbn; auto.
   apply Wf_term_alt in Ht. apply Ht.
 - rewrite map_length.
   destruct (funsymbs th f); [|easy].
   case eqb; [|easy].
   revert l. fix IH' 1. destruct l as [|t l]; cbn; auto.
   f_equal. apply IH. apply IH'.
Qed.

Lemma term_closure_level t (genv:variable->M) :
  level (term_closure genv t) = level t.
Proof.
 revert t.
 fix IH 1. destruct t as [ | | f l]; cbn; auto.
 - destruct (genv v) as (t,Ht); cbn; auto.
   apply Wf_term_alt in Ht. apply Ht.
 - revert l. fix IH' 1. destruct l as [|t l]; cbn; auto.
   f_equal. apply IH. apply IH'.
Qed.

Lemma empty_union s s' : Vars.Empty (Vars.union s s') <->
 Vars.Empty s /\ Vars.Empty s'.
Proof.
 split. split; varsdec. varsdec.
Qed.

Lemma term_closure_fclosed t (genv:variable->M) :
  FClosed (term_closure genv t).
Proof.
 revert t.
 fix IH 1. destruct t as [ | | f l]; cbn; auto.
 - destruct (genv v) as (t,Ht); cbn; auto.
   apply Wf_term_alt in Ht. apply Ht.
 - unfold FClosed in *. cbn.
   revert l. fix IH' 1. destruct l as [|t l]; cbn; auto.
   unfold term_closure in *.
   apply empty_union; auto.
Qed.

Lemma closure_check f genv :
 check th (closure genv f) = check th f.
Proof.
 induction f; cbn; auto.
 - rewrite map_length.
   destruct predsymbs; [|easy].
   case eqb; [|easy].
   revert l.
   induction l as [|t l]; cbn; auto. f_equal; auto.
   change (check th (term_closure genv t) = check th t). (* TODO *)
   apply term_closure_check.
 - unfold closure in *. now rewrite IHf1, IHf2.
Qed.

Lemma closure_level f (genv:variable->M) :
  level (closure genv f) = level f.
Proof.
 induction f; cbn; auto.
 revert l. induction l as [|t l IH]; cbn; auto.
 f_equal; auto.
 apply (term_closure_level t genv). (* TODO *)
Qed.

Lemma closure_fclosed f (genv:variable->M) :
  FClosed (closure genv f).
Proof.
 induction f; cbn; auto.
 - unfold FClosed in *. cbn.
   revert l. induction l as [|t l IH]; cbn; auto.
   apply empty_union; split; auto.
   apply (term_closure_fclosed t genv).
 - unfold FClosed in *. cbn.
   apply empty_union; split; auto.
Qed.

Lemma term_closure_wf t genv :
  check th t = true -> BClosed t ->
  Wf_term th (term_closure genv t).
Proof.
 repeat split.
 - now rewrite term_closure_check.
 - red. now rewrite term_closure_level.
 - apply term_closure_fclosed.
Qed.

Lemma term_closure_wf' t genv :
  check th t = true -> BClosed t ->
  wf_term th (term_closure genv t) = true.
Proof.
 intros CK BC. apply Wf_term_alt. now apply term_closure_wf.
Qed.

Lemma closure_wf f genv :
  check th f = true -> BClosed f ->
  Wf th (closure genv f).
Proof.
 repeat split.
 - now rewrite closure_check.
 - red. now rewrite closure_level.
 - apply closure_fclosed.
Qed.

Lemma closure_bsubst n t f genv :
 FClosed t ->
 closure genv (bsubst n t f) = bsubst n t (closure genv f).
Proof.
 unfold closure.
 intros FC.
 rewrite form_vmap_bsubst.
 f_equal.
 rewrite term_vmap_id; auto.
 intros v. red in FC. intuition.
 intros v. destruct (genv v) as (u,Hu); simpl.
 apply Wf_term_alt in Hu. apply Hu.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
Lemma interp_pred p l :
 check th (Pred p l) = true ->
 BClosed (Pred p l) ->
 forall genv,
   interp_form mo genv [] (Pred p l) <->
   IsTheorem Classic th
     (Pred p (map (fun t => proj1_sig (interp_term mo genv [] t)) l)).
Proof.
 unfold BClosed. cbn.
 destruct (predsymbs th p) as [n|] eqn:E; [|easy].
 rewrite lazy_andb_iff, eqb_eq. intros (L,CK) BC genv.
 unfold mk_preds; rewrite E. clear E.
 set (l0 := one_listterm th oneconst Honeconst n).
 rewrite build_map_arity with (any := l0) by now rewrite map_length.
 rewrite build_mk with (oneconst := oneconst) by (auto; now rewrite map_length).
 rewrite map_map; reflexivity.
Qed.

Lemma interp_term_carac t :
  check th t = true -> BClosed t ->
  forall genv,
    proj1_sig (interp_term mo genv [] t) = term_closure genv t.
Proof.
 induction t as [ | | f l IH] using term_ind'; cbn; auto.
 - unfold BClosed. cbn. easy.
 - destruct (funsymbs th f) as [n|] eqn:E; [|easy].
   rewrite lazy_andb_iff, eqb_eq.
   intros (L,CK) BC genv.
   unfold mk_funs.
   destruct rich_funs as ([(n',a)| ] & Ho & Ho'); cbn in *.
   2: congruence.
   assert (Hn : n' = n) by congruence.
   subst n'.
   rewrite Ho' by now rewrite map_length.
   clear Ho Ho'.
   rewrite map_map.
   f_equal. apply map_ext_iff.
   intros t Ht. apply IH; auto.
   + rewrite forallb_forall in CK; auto.
   + red in BC. cbn in BC. rewrite list_max_map_0 in BC; auto.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
459
460
461
462
463
464
465
466
Lemma interp_term_carac' (t:term) genv
  (CK : check th t = true) (BC : BClosed t) :
  interp_term mo genv [] t =
  exist _ (term_closure genv t) (term_closure_wf' t genv CK BC).
Proof.
 apply proof_irr. cbn. now apply interp_term_carac.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
Lemma complete' A : Wf th A ->
 IsTheorem Classic th (~A) <-> ~IsTheorem Classic th A.
Proof.
 split.
 - intros Thm' Thm. apply consistent.
   apply Thm_Not_e with A; auto.
 - destruct (complete A); trivial. now intros [ ].
Qed.

Lemma thm_and A B :
  IsTheorem Classic th A /\ IsTheorem Classic th B <->
  IsTheorem Classic th (A /\ B).
Proof.
 split.
 - intros ((WfA & axsA & FA & PRA), (WfB & axsB & FB & PRB)).
   split. now apply Op_wf.
   exists (axsA ++ axsB); split.
   + rewrite Forall_forall in *; intros x; rewrite in_app_iff;
     intros [ | ]; auto.
   + apply R_And_i.
     * clear PRB; eapply Pr_weakening; eauto. constructor.
       intros a. rewrite in_app_iff; auto.
     * eapply Pr_weakening; eauto. constructor.
       intros a. rewrite in_app_iff; auto.
 - intros (WF & axs & F & PR); rewrite Op_wf in WF. split.
   + split. easy.
     exists axs; split; auto.
     apply R_And_e1 with B; auto.
   + split. easy.
     exists axs; split; auto.
     apply R_And_e2 with A; auto.
Qed.

Lemma thm_or A B : Wf th (A\/B) ->
  IsTheorem Classic th A \/ IsTheorem Classic th B <->
  IsTheorem Classic th (A \/ B).
Proof.
 intros WF.
 split.
 - intros [(_ & axs & F & PR)|(_ & axs & F & PR)].
   + split; auto. exists axs; split; auto.
   + split; auto. exists axs; split; auto.
 - intros (_ & axs & F & PR); rewrite Op_wf in WF.
Pierre Letouzey's avatar
Pierre Letouzey committed
510
511
512
513
   destruct (complete A) as [HA|HA]; [easy|now left|].
   destruct HA as (WfA & axsA & FA & PRA).
   destruct (complete B) as [HB|HB]; [easy|now right|].
   destruct HB as (WfB & axsB & FB & PRB).
Pierre Letouzey's avatar
Pierre Letouzey committed
514
   destruct consistent.
Pierre Letouzey's avatar
Pierre Letouzey committed
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
   split. apply False_wf.
   exists (axs++axsA++axsB). split.
   rewrite Forall_forall in *; intros x; rewrite !in_app_iff;
     intros [|[ | ]]; auto.
   apply R_Or_e with A B.
   + clear PRA PRB; eapply Pr_weakening; eauto. constructor.
     intros a. rewrite in_app_iff; auto.
   + apply R_Not_e with A.
     * apply R'_Ax.
     * clear PR PRB; eapply Pr_weakening; eauto. constructor.
       intros a. simpl. rewrite !in_app_iff; auto.
   + apply R_Not_e with B.
     * apply R'_Ax.
     * clear PR PRA; eapply Pr_weakening; eauto. constructor.
       intros a. simpl. rewrite !in_app_iff; auto.
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
531
532


Pierre Letouzey's avatar
Pierre Letouzey committed
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
Lemma thm_impl A B : Wf th (A->B) ->
  (IsTheorem Classic th A -> IsTheorem Classic th B) <->
  IsTheorem Classic th (A -> B).
Proof.
 intros WF.
 split.
 - intros IM.
   destruct (complete A) as [HA|HA]; [rewrite Op_wf in WF; easy | | ].
   + specialize (IM HA).
     destruct IM as (WfB & axsB & FB & PRB).
     split; auto.
     exists axsB; split; auto.
     apply R_Imp_i.
     eapply Pr_weakening; eauto. constructor. intros a; simpl; auto.
   + destruct HA as (WfA & axsA & FA & PRA).
     split; auto.
     exists axsA; split; auto.
     apply R_Imp_i.
     apply R_Fa_e.
     apply R_Not_e with A. apply R'_Ax.
     eapply Pr_weakening; eauto. constructor. intros a; simpl; auto.
 - intros (_ & axsAB & FAB & PRAB) (_ & axsA & FA & PRA).
   split. now rewrite Op_wf in WF.
   exists (axsAB++axsA). split.
   rewrite Forall_forall in *; intros x; rewrite !in_app_iff;
     intros [|]; auto.
   apply R_Imp_e with A.
   + clear PRA; eapply Pr_weakening; eauto. constructor.
       intros a. simpl. rewrite !in_app_iff; auto.
   + clear PRAB; eapply Pr_weakening; eauto. constructor.
       intros a. simpl. rewrite !in_app_iff; auto.
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
565

Pierre Letouzey's avatar
Pierre Letouzey committed
566
567
Lemma pr_notex_allnot logic c A :
 Pr logic (c  ~A) <-> Pr logic (c  ~A).
Pierre Letouzey's avatar
Pierre Letouzey committed
568
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
 split.
 - intros NE.
   assert (Hx := fresh_var_ok (fvars (c  A))).
   set (x := fresh_var (fvars (c  A))) in *.
   apply R_All_i with x; cbn - [Vars.union] in *. varsdec.
   apply R_Not_i.
   apply R_Not_e with (A)%form.
   + apply R_Ex_i with (FVar x); auto using R'_Ax.
   + eapply Pr_weakening; eauto. constructor; red; simpl; auto.
 - intros AN.
   apply R_Not_i.
   assert (Hx := fresh_var_ok (fvars (c  A))).
   set (x := fresh_var (fvars (c  A))) in *.
   apply R'_Ex_e with x. cbn in *. varsdec.
   eapply R_Not_e; [apply R'_Ax|].
   eapply Pr_weakening. eapply R_All_e with (t:=FVar x); eauto.
   constructor. red; simpl; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
586
587
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
588
589
Lemma pr_notexnot c A :
 Pr Classic (c  ~~A) <-> Pr Classic (c  A).
Pierre Letouzey's avatar
Pierre Letouzey committed
590
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
 split.
 - intros NEN.
   assert (Hx := fresh_var_ok (fvars (c  A))).
   set (x := fresh_var (fvars (c  A))) in *.
   apply R_All_i with x; cbn - [Vars.union] in *. varsdec.
   apply R_Absu; auto.
   apply R_Not_e with (~A)%form.
   apply R_Ex_i with (FVar x); auto using R'_Ax.
   eapply Pr_weakening; eauto. constructor; red; simpl; auto.
 - intros ALL.
   apply R_Not_i.
   assert (Hx := fresh_var_ok (fvars (c  A))).
   set (x := fresh_var (fvars (c  A))) in *.
   apply R'_Ex_e with x. cbn in *. varsdec.
   cbn.
   eapply R_Not_e; [|eapply R'_Ax].
   eapply Pr_weakening. eapply R_All_e with (t:=FVar x); eauto.
   constructor. red; simpl; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
609
610
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
611
612
Lemma thm_notexnot A : Wf th (A) ->
  IsTheorem Classic th (~~A) <-> IsTheorem Classic th (A).
Pierre Letouzey's avatar
Pierre Letouzey committed
613
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
614
615
616
617
 intros WF.
 split; intros (_ & axs & F & P).
 - split; auto. exists axs; split; auto. now apply pr_notexnot.
 - split; auto. exists axs; split; auto. now apply pr_notexnot.
Pierre Letouzey's avatar
Pierre Letouzey committed
618
619
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
620
621
Lemma Wf_bsubst f t :
 Wf th (f) -> Wf_term th t -> Wf th (bsubst 0 t f).
Pierre Letouzey's avatar
Pierre Letouzey committed
622
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
623
624
625
626
627
628
 intros (CKf & BCf & FCf) (CKt & BCt & FCt).
 repeat split.
 - apply check_bsubst; auto.
 - apply Nat.le_0_r.
   apply level_bsubst; red in BCf; red in BCt; cbn in *; omega.
 - unfold FClosed in *. rewrite bsubst_fvars. varsdec.
Pierre Letouzey's avatar
Pierre Letouzey committed
629
630
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
631
632
Lemma thm_all_e logic A t : Wf_term th t ->
 IsTheorem logic th (A) -> IsTheorem logic th (bsubst 0 t A).
Pierre Letouzey's avatar
Pierre Letouzey committed
633
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
634
635
636
637
 intros WFt (WFA & axs & F & P).
 split. apply Wf_bsubst; auto.
 exists axs. split; auto.
 apply R_All_e; auto. apply WFt.
Pierre Letouzey's avatar
Pierre Letouzey committed
638
639
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
640
641
642
Lemma thm_ex_i logic A t : Wf th (A) -> Wf_term th t ->
 IsTheorem logic th (bsubst 0 t A) ->
 IsTheorem logic th (A).
Pierre Letouzey's avatar
Pierre Letouzey committed
643
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
644
645
646
647
 intros WFA WFt (_ & axs & F & P).
 split; auto.
 exists axs. split; auto.
 apply R_Ex_i with t; auto. apply WFt.
Pierre Letouzey's avatar
Pierre Letouzey committed
648
649
650
Qed.


Pierre Letouzey's avatar
Pierre Letouzey committed
651
652
653
654
655
656
657
658
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
659
660
661
662
663
664
665
Lemma height_bsubst n t f :
 height (bsubst n t f) = height f.
Proof.
 revert n.
 induction f; cbn; f_equal; auto.
Qed.

Pierre Letouzey's avatar
Pierre Letouzey committed
666
667
668
669
670
671
672
673
674
675
676
677
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.

Pierre Letouzey's avatar
Pierre Letouzey committed
678
Lemma interp_carac f : check th f = true -> BClosed f ->
Pierre Letouzey's avatar
Pierre Letouzey committed
679
680
681
682
 forall genv,
   interp_form mo genv [] f <->
     IsTheorem Classic th (closure genv f).
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
683
684
 induction f as [h IH f Hf] using height_ind. destruct f; intros CK BC genv.
 - clear IH Hf. cbn.
Pierre Letouzey's avatar
Pierre Letouzey committed
685
686
   unfold IsTheorem. intuition.
   now exists [].
Pierre Letouzey's avatar
Pierre Letouzey committed
687
 - clear IH Hf. cbn.
Pierre Letouzey's avatar
Pierre Letouzey committed
688
   unfold IsTheorem. intuition.
Pierre Letouzey's avatar
Pierre Letouzey committed
689
   apply consistent; split; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
690
691
 - clear IH Hf.
   rewrite interp_pred; auto. simpl.
Pierre Letouzey's avatar
Pierre Letouzey committed
692
693
694
695
696
697
698
699
700
701
   unfold vmap, vmap_list.
   assert (forall t, In t l ->
            proj1_sig (interp_term mo genv [] t) =
            term_vmap (fun v : variable => proj1_sig (genv v)) t).
   { intros t Ht. apply interp_term_carac.
     cbn in CK.
     destruct predsymbs; [|easy]. destruct eqb; [|easy].
     rewrite forallb_forall in CK; auto.
     red in BC. cbn in BC. rewrite list_max_map_0 in BC; auto. }
   apply map_ext_iff in H. rewrite H. reflexivity.
Pierre Letouzey's avatar
Pierre Letouzey committed
702
 - simpl. rewrite IH; auto with arith.
Pierre Letouzey's avatar
Pierre Letouzey committed
703
704
   symmetry. apply complete'.
   apply closure_wf; auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
705
 - cbn in *. rewrite lazy_andb_iff in CK. destruct CK as (CK1,CK2).
Pierre Letouzey's avatar
Pierre Letouzey committed
706
   red in BC. cbn in BC. apply max_0 in BC. destruct BC as (BC1,BC2).
Pierre Letouzey's avatar
Pierre Letouzey committed
707
708
709
710
   destruct o; simpl; rewrite !IH; auto; try omega with *.
   + apply thm_and.
   + apply thm_or. apply Op_wf. split; apply (closure_wf _ genv); auto.
   + apply thm_impl. apply Op_wf. split; apply (closure_wf _ genv); auto.
Pierre Letouzey's avatar
Pierre Letouzey committed
711
 - simpl.
Pierre Letouzey's avatar
Pierre Letouzey committed
712
713
714
715
   destruct q; split.
   + intros H.
     destruct (complete (closure genv (~f))); [apply closure_wf; auto| | ].
     * destruct (witsat (closure genv (~f)) H0) as (c & Hc & Thm).
Pierre Letouzey's avatar
Pierre Letouzey committed
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
       rewrite <- closure_bsubst in Thm by auto.
       change (closure _ _) with (~closure genv (bsubst 0 (Cst c) f))%form in Thm.
       assert (check th (bsubst 0 (Cst c) f) = true).
       { apply check_bsubst; cbn; auto. now rewrite Hc, eqb_refl. }
       assert (BClosed (bsubst 0 (Cst c) f)).
       { apply Nat.le_0_r, level_bsubst; auto.
         cbn. red in BC; cbn in BC. omega. }
       rewrite complete' in Thm by (apply closure_wf; auto).
       rewrite <- IH in Thm; auto.
       { rewrite <- interp_form_bsubst0 in Thm; auto.
         destruct Thm. apply H.
         cbn. red in BC; cbn in BC. omega. }
       { rewrite height_bsubst. cbn. cbn in Hf. omega. }
     * apply thm_notexnot; auto.
       apply (closure_wf ( f) genv); auto.
   + intros Thm (t,Ht).
     rewrite interp_form_bsubst0 with (u:=t).
     2:{ red in BC. cbn in BC. omega. }
     2:{ apply Wf_term_alt in Ht. apply Ht. }
     2:{ destruct (proj2 (Wf_term_alt _ _) Ht) as (CKt & BCt & FCt).
         rewrite (interp_term_carac' t genv CKt BCt).
         apply proof_irr. cbn. apply term_vmap_id. intros v.
         red in FCt. intuition. }
     apply Wf_term_alt in Ht.
     rewrite IH.
     { rewrite closure_bsubst by apply Ht.
       apply thm_all_e; auto. }
     { rewrite height_bsubst. cbn in Hf. omega. }
     { rewrite check_bsubst; auto. apply Ht. }
     { apply Nat.le_0_r. apply level_bsubst. red in BC.
       cbn in BC. omega. apply Nat.le_0_r, Ht. }
   + intros ((t,Ht),Int).
     rewrite interp_form_bsubst0 with (u:=t) in Int.
     2:{ red in BC. cbn in BC. omega. }
     2:{ clear Int.
         apply Wf_term_alt in Ht. apply Ht. }
     2:{ clear Int.
         destruct (proj2 (Wf_term_alt _ _) Ht) as (CKt & BCt & FCt).
         rewrite (interp_term_carac' t genv CKt BCt).
         apply proof_irr. cbn. apply term_vmap_id. intros v.
         red in FCt. intuition. }
     apply Wf_term_alt in Ht.
     rewrite IH in Int.
     { rewrite closure_bsubst in Int by apply Ht.
       apply thm_ex_i with t; auto.
       apply (closure_wf (f) genv); auto. }
     { rewrite height_bsubst. cbn in Hf. omega. }
     { rewrite check_bsubst; auto. apply Ht. }
     { apply Nat.le_0_r. apply level_bsubst. red in BC.
       cbn in BC. omega. apply Nat.le_0_r, Ht. }
   + intros Thm.
     destruct (witsat (closure genv f) Thm) as (c & Hc & Thm').
     rewrite <- closure_bsubst in Thm' by auto.
     rewrite <- IH in Thm'.
     2:{ rewrite height_bsubst. cbn in Hf. omega. }
     2:{ rewrite check_bsubst; auto. cbn. now rewrite Hc, eqb_refl. }
     2:{ apply Nat.le_0_r. apply level_bsubst. red in BC.
         cbn in BC. omega. auto. }
     exists (exist _ (Cst c) (Cst_wf' th c Hc)).
     rewrite interp_form_bsubst0; eauto.
     { red in BC. cbn in BC. omega. }
     { apply proof_irr. rewrite interp_term_carac; auto.
       cbn. now rewrite Hc, eqb_refl. }
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
780

Pierre Letouzey's avatar
Pierre Letouzey committed
781
782
Lemma interp_carac_closed f genv : Wf th f ->
 interp_form mo genv [] f <-> IsTheorem Classic th f.
Pierre Letouzey's avatar
Pierre Letouzey committed
783
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
784
785
786
787
788
789
 intros WF.
 replace f with (closure genv f) at 2.
 apply interp_carac; apply WF.
 apply form_vmap_id. intros v. destruct WF as (_ & _ & FC).
 red in FC. intuition.
Qed.
Pierre Letouzey's avatar
Pierre Letouzey committed
790
791
792

Lemma axioms_ok A :
  IsAxiom th A ->
Pierre Letouzey's avatar
Pierre Letouzey committed
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
  forall genv, interp_form mo genv [] A.
Proof.
 intros HA genv. apply interp_carac_closed.
 apply WfAxiom; auto.
 apply ax_thm; auto.
Qed.

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

End SyntacticModel.

Lemma premodel_restrict sign sign' M :
 SignExtend sign sign' ->
 PreModel M sign' -> PreModel M sign.
Proof.
 intros SE mo.
 set (fs := fun f => match sign.(funsymbs) f with
                     | None => None
                     | _ => mo.(funs) f
                     end).
 set (ps := fun f => match sign.(predsymbs) f with
                     | None => None
                     | _ => mo.(preds) f
                     end).
 apply Build_PreModel with fs ps.
 - exact mo.(someone).
 - intros f. unfold fs.
   generalize (mo.(funsOk) f).
   destruct SE as (SE,_). unfold optfun_finer,opt_finer in SE.
   destruct (SE f) as [-> | ->]; auto.
   destruct (funsymbs sign' f); auto.
 - intros p. unfold ps.
   generalize (mo.(predsOk) p).
   destruct SE as (_,SE). unfold optfun_finer,opt_finer in SE.
   destruct (SE p) as [-> | ->]; auto.
   destruct (predsymbs sign' p); auto.
Defined.

Lemma model_restrict logic th th' M :
 Extend logic th th' -> Model M th' -> Model M th.
Proof.
 intros (SE,EX) (mo,AxOk).
 apply Build_Model with (premodel_restrict th th' M SE mo).
 intros A HA genv.
Pierre Letouzey's avatar
Pierre Letouzey committed
839
840
Admitted.

Pierre Letouzey's avatar
Pierre Letouzey committed
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
Lemma consistent_has_model (th:theory) (nc : NewCsts th) :
 MyExcludedMiddle Classic ->
 Consistent Classic th ->
 { M & Model M th }.
Proof.
 intros EM C.
 set (th' := supercomplete Classic th nc).
 exists (closed_term th').
 apply (model_restrict Classic th th').
 apply supercomplete_extend.
 apply SyntacticModel with (oneconst := nc 0).
 - apply supercomplete_consistent; auto.
 - apply supercomplete_complete; auto.
 - 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,
   Wf th T ->
   (forall M (mo : Model M th) genv, interp_form mo genv [] T)
   -> IsTheorem Classic th T.
Proof.
 intros EM T WF HT.
 destruct (EM (IsTheorem Classic th False))
   as [(_ & axs & F & P)|C].
 - split; auto. exists axs; auto.
 - change (Consistent Classic th) in C.
   destruct (EM (IsTheorem Classic th T)) as [Thm|NT]; auto.
   exfalso.
   assert (WF' : forall A, A = (~T)%form \/ IsAxiom th A -> Wf th A).
   { intros A [->|HA]; auto using WfAxiom. }
   set (th' := {| sign := th;
                 IsAxiom := fun f => f = (~T)%form \/ IsAxiom th f;
                 WfAxiom := WF' |}).
   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. }
   assert (Consistent Classic th').
   { intros (_ & axs & F & P).
     (* soit ~T dans axs et donc on prouve T contradiction
        soit pas et on infirme la consistence de th *)
     admit. }
   destruct (consistent_has_model th' nc') as (M,mo); auto.
   + red; intros. apply EM.
   + (* model interprete T as 0 (car ~T axiome de th' *)
     apply (model_restrict Classic th) in mo.
Admitted.