-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathHenkin2FOL.v
1914 lines (1621 loc) · 92.9 KB
/
Henkin2FOL.v
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
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
187
188
189
190
191
192
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
220
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
271
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
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
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
459
460
461
462
463
464
465
466
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
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
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
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
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
780
781
782
783
784
785
786
787
788
789
790
791
792
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
839
840
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
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(** * Reduction to FOL *)
Require Import FOL SOL FullSyntax Tarski Henkin Deduction.
Require Import Vector VectorLib Util.
Require Import Equations.Equations Equations.Prop.DepElim.
Require Import Lia.
Require Import Enumerable Decidable.
Import VectorNotations.
Import SubstNotations.
Definition toFOLBinop b := match b with
| FullSyntax.Conj => FOL.Conj
| FullSyntax.Disj => FOL.Disj
| FullSyntax.Impl => FOL.Impl
end.
Definition toSOLBinop b := match b with
| FOL.Conj => FullSyntax.Conj
| FOL.Disj => FullSyntax.Disj
| FOL.Impl => FullSyntax.Impl
end.
Definition toSOLQuantop b := match b with
| FOL.All => FullSyntax.All
| FOL.Ex => FullSyntax.Ex
end.
Definition toFOLQuantop b := match b with
| FullSyntax.All => FOL.All
| FullSyntax.Ex => FOL.Ex
end.
Lemma toSOLBinop_toFOLBinop b :
toSOLBinop (toFOLBinop b) = b.
Proof.
now destruct b.
Qed.
Section Signature.
Context {Σf2 : SOL.funcs_signature}.
Context {Σp2 : SOL.preds_signature}.
(* Add symbols for predicate application to the SOL signature. *)
Inductive FOLSyms :=
| NormalSym : syms -> FOLSyms.
Inductive FOLPreds :=
| NormalPred : preds -> FOLPreds
| PredApp : nat -> FOLPreds.
Instance Σf1 : FOL.funcs_signature := {|
FOL.syms := FOLSyms ;
FOL.ar_syms f := match f with NormalSym f => SOL.ar_syms f end
|}.
Instance Σp1 : FOL.preds_signature := {|
FOL.preds := FOLPreds ;
FOL.ar_preds P := match P with NormalPred P => SOL.ar_preds P | PredApp ar => S ar end
|}.
(** The extended signatures preserve discreteness and enumerablility *)
Lemma Sigma_f1_eq_dec :
eq_dec Σf2 -> eq_dec Σf1.
Proof.
intros H [x] [y]. enough (dec (x = y)) as [->|H1].
now left. right. congruence. apply H.
Qed.
Lemma Sigma_p1_eq_dec :
eq_dec Σp2 -> eq_dec Σp1.
Proof.
intros H [p|n] [p'|n'].
- enough (dec (p = p')) as [->|H1]. now left. right. congruence. apply H.
- right. congruence.
- right. congruence.
- decide (n = n') as [->|]. now left. right. congruence.
Qed.
Lemma Sigma_f1_enumerable :
enumerable__T Σf2 -> enumerable__T Σf1.
Proof.
intros [f Hf]. exists (fun n => match f n with Some x => Some (NormalSym x) | None => None end).
intros [x]. destruct (Hf x) as [n H]. exists n. now rewrite H.
Qed.
Lemma Sigma_p1_enumerable :
enumerable__T Σp2 -> enumerable__T Σp1.
Proof.
intros [f Hf].
exists (fun n => match pi1 n with
| 0 => match f (pi2 n) with Some x => Some (NormalPred x) | None => None end
| _ => Some (PredApp (pi2 n))
end).
intros [x|n].
- destruct (Hf x) as [n H]. exists (embed (0,n)). now rewrite pi1_correct, pi2_correct, H.
- exists (embed (1,n)). now rewrite pi1_correct, pi2_correct.
Qed.
(** Notations for first-order syntax *)
Notation "⊥'" := FOL.falsity.
Notation "A ∧' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Conj A B) (at level 41).
Notation "A ∨' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Disj A B) (at level 42).
Notation "A '-->'' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Impl A B) (at level 43, right associativity).
Notation "A '<-->'' B" := ((A -->' B) ∧' (B -->' A)) (at level 44, right associativity).
Notation "∀' Phi" := (@FOL.quant Σf1 Σp1 FOL.full_operators _ FOL.All Phi) (at level 50).
Notation "∃' Phi" := (@FOL.quant Σf1 Σp1 FOL.full_operators _ FOL.Ex Phi) (at level 50).
Notation "phi `[ sigma ]" := (FOL.subst_form sigma phi) (at level 7, left associativity, format "phi '/' `[ sigma ]") : subst_scope.
Notation "f >>' g" := (FOL.funcomp g f) (at level 50) : subst_scope.
Notation "s '..''" := (FOL.scons s FOL.var) (at level 4, format "s ..'") : subst_scope.
Notation "↑'" := (S >>' FOL.var) : subst_scope.
Notation "A ⊢1 phi" := (FOL.prv _ A phi) (at level 61).
Notation "A ⊢2 phi" := (Deduction.prv A phi) (at level 61).
Lemma FOL_term_ind (p : FOL.term -> Prop) :
(forall x, p (FOL.var x)) -> (forall F v (IH : VectorLib.Forall p v), p (FOL.func F v)) -> forall t, p t.
Proof.
intros f1 f2. fix F 1. intros [n|f v].
- apply f1.
- apply f2. induction v. easy. split. apply F. apply IHv.
Qed.
(** ** Definition of Translation Function *)
(** The idea is to use functions pos_i, pos_f and pos_p that given a
position in the SOL environment tell us the positition of the same
object in the FOL environment.
Quantifiers update those mappings by adding 0 the the matching
kind and shiftig the other two. *)
Definition pcons (pos : nat -> nat) : nat -> nat :=
fun n => match n with 0 => 0 | S n => S (pos n) end.
Definition pcons' (ar : nat) (pos : nat -> nat -> nat) : nat -> nat -> nat :=
fun n ar' => match n with
| 0 => if PeanoNat.Nat.eq_dec ar ar' then 0 else S (pos 0 ar')
| S n => if PeanoNat.Nat.eq_dec ar ar' then S (pos n ar') else S (pos (S n) ar') end.
Definition pshift (pos : nat -> nat) : nat -> nat := fun n => S (pos n).
Definition pshift' (pos : nat -> nat -> nat) : nat -> nat -> nat := fun n ar => S (pos n ar).
Fixpoint toFOLTerm (pos_i : nat -> nat) (t : SOL.term) : FOL.term := match t with
| SOL.var_indi x => FOL.var (pos_i x)
| SOL.func (var_func x ar) v => FOL.var 0
| SOL.func (sym f) v => FOL.func (NormalSym f) (Vector.map (toFOLTerm pos_i) v)
end.
Fixpoint toFOLForm (pos_i : nat -> nat) (pos_p : nat -> nat -> nat) (phi : SOL.form) : FOL.form := match phi with
| SOL.fal => FOL.falsity
| SOL.atom (pred P) v => FOL.atom (NormalPred P) (Vector.map (toFOLTerm pos_i) v)
| SOL.atom (var_pred x ar) v => FOL.atom (PredApp ar) (FOL.var (pos_p x ar) :: Vector.map (toFOLTerm pos_i) v)
| SOL.bin op phi psi => FOL.bin (toFOLBinop op) (toFOLForm pos_i pos_p phi) (toFOLForm pos_i pos_p psi)
| SOL.quant_indi op phi => FOL.quant (toFOLQuantop op) (toFOLForm (pcons pos_i) (pshift' pos_p) phi)
| SOL.quant_func op ar phi => FOL.falsity
| SOL.quant_pred op ar phi => FOL.quant (toFOLQuantop op) (toFOLForm (pshift pos_i) (pcons' ar pos_p) phi)
end.
Definition initial_pos_i n := embed (0, n).
Definition initial_pos_p n ar := embed (1, embed (n, ar)).
Definition toFOLForm' (phi : SOL.form) := toFOLForm initial_pos_i initial_pos_p phi.
Lemma toFOLTerm_ext_i pos_i pos_i' t :
(forall n, ~bounded_indi_term n t -> pos_i n = pos_i' n)
-> toFOLTerm pos_i t = toFOLTerm pos_i' t.
Proof.
intros Hi. induction t; cbn.
- rewrite Hi. reflexivity. cbn; lia.
- reflexivity.
- f_equal. apply map_ext_in. intros t H. eapply Forall_in in IH. apply IH.
intros n H1. apply Hi. intros H2. apply H1. eapply Forall_in in H2. apply H2. all: easy.
Qed.
Lemma toFOLForm_ext_i pos_i pos_i' pos_p phi :
(forall n, ~bounded_indi n phi -> pos_i n = pos_i' n)
-> toFOLForm pos_i pos_p phi = toFOLForm pos_i' pos_p phi.
Proof.
induction phi in pos_i, pos_i', pos_p |-*; cbn; intros Hi.
- reflexivity.
- destruct p; cbn; f_equal. f_equal. all: apply map_ext_in; intros t H;
apply toFOLTerm_ext_i; intros n' H1; apply Hi; intros H2; apply H1;
eapply Forall_in in H2; try apply H2; easy.
- erewrite IHphi1, IHphi2; firstorder.
- f_equal. apply IHphi. intros [] H; cbn. reflexivity. now rewrite Hi.
- reflexivity.
- f_equal. apply IHphi. intros n' H. unfold pshift. now rewrite Hi.
Qed.
Lemma toFOLForm_ext_p pos_i pos_p pos_p' phi :
(forall n ar, ~bounded_pred ar n phi -> pos_p n ar = pos_p' n ar)
-> toFOLForm pos_i pos_p phi = toFOLForm pos_i pos_p' phi.
Proof.
induction phi in pos_i, pos_p, pos_p' |-*; intros Hp; cbn.
- reflexivity.
- destruct p; f_equal. rewrite Hp. reflexivity. cbn; lia.
- erewrite IHphi1, IHphi2; firstorder.
- erewrite IHphi. reflexivity. intros n ar H. unfold pshift'. now rewrite Hp.
- reflexivity.
- erewrite IHphi. reflexivity. intros [] ar H; cbn; destruct PeanoNat.Nat.eq_dec as [->|].
reflexivity. all: rewrite Hp; try reflexivity; cbn; now intros [[]|[]]; try lia.
Qed.
Definition closed phi := bounded_indi 0 phi /\ (forall ar, bounded_func ar 0 phi) /\ (forall ar, bounded_pred ar 0 phi).
Lemma toFOLForm_closed_ext pos_i pos_p pos_i' pos_p' phi :
closed phi -> toFOLForm pos_i pos_p phi = toFOLForm pos_i' pos_p' phi.
Proof.
intros C. erewrite toFOLForm_ext_p, toFOLForm_ext_i. reflexivity.
- intros n H. exfalso. apply H. eapply bounded_indi_up. 2: apply C. lia.
- intros n ar H. exfalso. apply H. eapply bounded_pred_up. 2: apply C. lia.
Qed.
Lemma comprehension_form_funcfree ar phi :
funcfree phi -> funcfree (comprehension_form ar phi).
Proof.
intros H. apply forall_n_funcfree. repeat split; cbn.
1,4: induction ar; firstorder. all: now apply funcfree_subst_p.
Qed.
Definition C := fun phi => exists ar psi, funcfree psi /\ phi = close All (comprehension_form ar psi).
Definition toFOLTheory (T : SOL.form -> Prop) := fun phi => exists phi', phi = toFOLForm' phi' /\ T phi'.
Lemma toFOLTheory_enumerable T :
enumerable T -> enumerable (toFOLTheory T).
Proof.
intros [f Hf]. exists (fun n => match f n with Some phi => Some (toFOLForm' phi) | None => None end).
intros phi. split.
- intros [psi [-> H]]. apply Hf in H as [n H]. exists n. now rewrite H.
- intros [n H]. destruct f eqn:H1.
+ inversion H. eexists. split. reflexivity. apply Hf. now exists n.
+ easy.
Qed.
Lemma C_enumerable :
enumerable__T Σf2 -> enumerable__T Σp2 -> enumerable C.
Proof.
intros E1 E2. unfold C. destruct form_enumerable as [f Hf]; trivial.
apply enumT_binop. apply enumT_quantop.
exists (fun n => match f (pi1 n) with Some phi => if funcfree_dec phi then Some (close All (comprehension_form (pi2 n) phi)) else None | None => None end).
intros phi. split.
- intros [ar [psi [H1 H2]]]. destruct (Hf psi) as [n H3].
exists (embed (n, ar)). rewrite pi1_correct, pi2_correct, H2, H3.
now destruct funcfree_dec.
- intros [n H1]. destruct f eqn:H2; try easy. destruct funcfree_dec; try easy.
inversion H1. eauto.
Qed.
(** ** Semantic Reduction *)
(** *** Translate Henkin Model to First-Order Model. *)
Section HenkinModel_To_FOModel.
Variable D2 : Type.
Context {I2 : Tarski.interp D2}.
Variable funcs : forall ar, (vec D2 ar -> D2) -> Prop.
Variable preds : forall ar, (vec D2 ar -> Prop) -> Prop.
Inductive D1 :=
| fromIndi : D2 -> D1
| fromPred : forall ar (P : vec D2 ar -> Prop), preds ar P -> D1.
Hypothesis D2_inhabited : D2.
Hypothesis funcs_inhabited : forall ar, { f | funcs ar f }.
Hypothesis preds_inhabited : forall ar, { P | preds ar P }.
Definition error_i := D2_inhabited.
Definition error_p ar := proj1_sig (preds_inhabited ar).
Lemma error_p_included ar :
preds ar (error_p ar).
Proof.
unfold error_p. now destruct preds_inhabited.
Qed.
Definition toIndi (d1 : D1) := match d1 with fromIndi d2 => d2 | _ => error_i end.
Definition toPred ar (d1 : D1) := match d1 with
| fromPred ar' P2 _ => match PeanoNat.Nat.eq_dec ar ar' with
| left e => match eq_sym e in _ = ar return vec D2 ar -> Prop with eq_refl => P2 end
| right _ => error_p ar
end
| _ => error_p ar
end.
Instance I1 : FOL.interp D1 := {|
FOL.i_func f := match f with
| NormalSym f => fun v => fromIndi (Tarski.i_f _ f (Vector.map toIndi v))
end ;
FOL.i_atom P := match P with
| NormalPred P => fun v => Tarski.i_P _ P (Vector.map (fun d => match d with fromIndi d => d | _ => error_i end) v)
| PredApp ar => fun v => match Vector.hd v with
| fromPred ar' P _ => match PeanoNat.Nat.eq_dec ar ar' with
| left e => P match e in _ = ar' return vec _ ar' with eq_refl => Vector.map toIndi (Vector.tl v) end
| right _ => error_p ar (Vector.map toIndi (Vector.tl v))
end
| _ => error_p ar (Vector.map toIndi (Vector.tl v))
end
end
|}.
Lemma toFOLTerm_correct_2To1 rho1 rho2 pos_i t :
funcfreeTerm t
-> (forall n, toIndi (rho1 (pos_i n)) = get_indi rho2 n)
-> toIndi (FOL.eval rho1 (toFOLTerm pos_i t)) = Tarski.eval D2 rho2 t.
Proof.
intros F Hi. induction t; cbn.
- apply Hi.
- now exfalso.
- f_equal. f_equal. rewrite !map_map. eapply map_ext_forall, Forall_ext_Forall.
apply IH. apply F.
Qed.
Ltac destruct_eq_dec :=
repeat (cbn; try rewrite nat_eq_dec_same; cbn; try destruct PeanoNat.Nat.eq_dec as [->|]; try destruct PeanoNat.Nat.eq_dec as [<-|]).
Lemma toFOLForm_correct_2To1 rho1 rho2 pos_i pos_p phi :
funcfree phi
-> (forall n, toIndi (rho1 (pos_i n)) = get_indi rho2 n)
-> (forall n ar, toPred ar (rho1 (pos_p n ar)) = get_pred rho2 n ar)
-> FOL.sat rho1 (toFOLForm pos_i pos_p phi) <-> Henkin.sat funcs preds rho2 phi.
Proof.
revert rho1 rho2 pos_i pos_p. induction phi; intros rho1 rho2 pos_i pos_p F Hi Hp; cbn.
- reflexivity.
- destruct p; cbn.
+ rewrite <- Hp.
assert (map toIndi (map (FOL.eval rho1) (map (toFOLTerm pos_i) v)) = map (eval D2 rho2) v) as ->. {
rewrite !map_map. eapply map_ext_forall, Forall_in.
intros t H. erewrite toFOLTerm_correct_2To1. reflexivity.
eapply Forall_in in F. apply F. easy. apply Hi. }
destruct (rho1 (pos_p n ar)); try easy. cbn. now destruct PeanoNat.Nat.eq_dec as [<-|].
+ assert (forall x y, x = y -> x <-> y) as X by now intros x y ->. apply X; clear X.
f_equal. rewrite !map_map. eapply map_ext, Forall2_identical, Forall_in.
intros t H. rewrite <- (toFOLTerm_correct_2To1 rho1 _ pos_i). now destruct FOL.eval.
eapply Forall_in in F. apply F. easy. apply Hi.
- specialize (IHphi1 rho1 rho2 pos_i pos_p ltac:(firstorder) ltac:(firstorder) ltac:(firstorder));
specialize (IHphi2 rho1 rho2 pos_i pos_p ltac:(firstorder) ltac:(firstorder) ltac:(firstorder)).
destruct b; cbn; tauto.
- destruct q; cbn; split.
+ intros H d. eapply IHphi. 4: apply (H (fromIndi d)). easy. intros []. all: firstorder.
+ intros H [d|ar P ?].
* eapply IHphi. 4: apply (H d). easy. intros []. all: firstorder.
* eapply IHphi. 4: apply (H error_i). easy. intros []. all: firstorder.
+ intros [[d|ar P ?] H].
* exists d. eapply IHphi. 4: apply H. easy. intros []. all: firstorder.
* exists error_i. eapply IHphi. 4: apply H. easy. intros []. all: firstorder.
+ intros [d H]. exists (fromIndi d). eapply IHphi. 4: apply H. easy. intros []. all: firstorder.
- now exfalso.
- destruct q; cbn; split.
+ intros H P HP'. eapply IHphi. 4: apply (H (fromPred _ P HP')). 3: intros [] ar'; destruct_eq_dec. all: firstorder.
+ intros H [d|ar P ?].
* eapply IHphi. 4: apply (H (error_p _)), error_p_included. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
* destruct (PeanoNat.Nat.eq_dec n ar) as [->|].
-- eapply IHphi. 4: apply (H P). 3: intros [] ar'; destruct_eq_dec. all: firstorder.
-- eapply IHphi. 4: apply (H (error_p _)), error_p_included. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
+ intros [[d|ar P HP'] H].
* exists (error_p _), (error_p_included _). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
* destruct (PeanoNat.Nat.eq_dec n ar) as [->|].
-- exists P, HP'. eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
-- exists (error_p _), (error_p_included _). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
+ intros [P [HP' H]]. exists (fromPred _ P HP'). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
Qed.
Definition toFOLEnv rho2 (H : henkin_env funcs preds rho2) := fun n => match unembed n with
| (0, n) => fromIndi (get_indi rho2 n)
| (_, x) => fromPred _ (get_pred rho2 (pi1 x) (pi2 x)) ltac:(apply H)
end.
Lemma toFOLEnv_correct_i rho2 (H : henkin_env funcs preds rho2) :
forall n, toIndi (toFOLEnv rho2 H (initial_pos_i n)) = get_indi rho2 n.
Proof.
intros n. unfold toFOLEnv, initial_pos_i. now rewrite unembed_embed.
Qed.
Lemma toFOLEnv_correct_p rho2 (H : henkin_env funcs preds rho2) :
forall n ar, toPred ar (toFOLEnv rho2 H (initial_pos_p n ar)) = get_pred rho2 n ar.
Proof.
intros n ar. unfold toFOLEnv, initial_pos_p.
rewrite unembed_embed, pi1_correct, pi2_correct.
destruct H. cbn. now rewrite nat_eq_dec_same.
Qed.
Lemma toFOLForm_correct_2To1' rho2 (H : henkin_env funcs preds rho2) phi :
funcfree phi -> FOL.sat (toFOLEnv rho2 H) (toFOLForm' phi) <-> Henkin.sat funcs preds rho2 phi.
Proof.
intros F. apply toFOLForm_correct_2To1. apply F.
apply toFOLEnv_correct_i. apply toFOLEnv_correct_p.
Qed.
End HenkinModel_To_FOModel.
(** *** Translate First-Order Model to Henkin Model. *)
Section FOModel_To_HenkinModel.
Variable D1 : Type.
Context {I1 : FOL.interp D1}.
Definition D2 := D1.
Definition funcs ar (f : vec D2 ar -> D2) := True.
Definition preds ar (P : vec D2 ar -> Prop) :=
exists d : D1, forall v, P v <-> i_atom (P:=PredApp ar) (d::v).
Instance I2 : Tarski.interp D2 := {|
Tarski.i_f f v := i_func (f:=NormalSym f) v ;
Tarski.i_P P v := i_atom (P:=NormalPred P) v
|}.
Lemma toFOLTerm_correct_1To2 rho1 rho2 pos_i t :
funcfreeTerm t
-> (forall n, get_indi rho2 n = rho1 (pos_i n))
-> Tarski.eval D2 rho2 t = FOL.eval rho1 (toFOLTerm pos_i t).
Proof.
intros F Hi. induction t; cbn.
- apply Hi.
- now exfalso.
- f_equal. rewrite map_map. eapply map_ext_forall, Forall_ext_Forall.
apply IH. apply F.
Qed.
Ltac destruct_eq_dec :=
repeat (cbn; try rewrite nat_eq_dec_same; cbn; try destruct PeanoNat.Nat.eq_dec as [->|]; try destruct PeanoNat.Nat.eq_dec as [<-|]).
Lemma toFOLForm_correct_1To2 rho1 rho2 pos_i pos_p phi :
funcfree phi
-> (forall n, get_indi rho2 n = rho1 (pos_i n))
-> (forall n ar, forall v, get_pred rho2 n ar v <-> i_atom (P:=PredApp ar) (rho1 (pos_p n ar) :: v))
-> FOL.sat rho1 (toFOLForm pos_i pos_p phi) <-> Henkin.sat funcs preds rho2 phi.
Proof.
revert rho1 rho2 pos_i pos_p. induction phi; intros rho1 rho2 pos_i pos_p F Hi Hp; cbn.
- reflexivity.
- destruct p; cbn.
+ rewrite <- Hp. assert (forall x y, x = y -> x <-> y) as X by now intros x y ->. apply X; clear X.
f_equal. rewrite !map_map. eapply map_ext_forall, Forall_in. intros t H.
erewrite <- toFOLTerm_correct_1To2. reflexivity.
eapply Forall_in in F. apply F. easy. apply Hi.
+ assert (forall x y, x = y -> x <-> y) as X by now intros x y ->. apply X; clear X.
f_equal. rewrite !map_map. eapply map_ext_forall, Forall_in. intros t H.
erewrite <- toFOLTerm_correct_1To2. reflexivity.
eapply Forall_in in F. apply F. easy. apply Hi.
- destruct F as [F1 F2]. specialize (IHphi1 rho1 rho2 pos_i pos_p F1 Hi Hp);
specialize (IHphi2 rho1 rho2 pos_i pos_p F2 Hi Hp). destruct b; cbn; tauto.
- destruct q; cbn; split.
+ intros H d. eapply IHphi. 4: apply (H d). easy. intros []. all: trivial; apply Hi.
+ intros H d. eapply IHphi. 4: apply (H d). easy. intros []. all: trivial; apply Hi.
+ intros [d H]. exists d. eapply IHphi. 4: apply H. easy. intros []. all: trivial; apply Hi.
+ intros [d H]. exists d. eapply IHphi. 4: apply H. easy. intros []. all: trivial; apply Hi.
- now exfalso.
- destruct q; cbn; split.
+ intros H P [d Hd]. eapply IHphi. 4: apply (H d). 3: intros [] ar'; destruct_eq_dec. all: try easy.
+ intros H d. eapply IHphi. 4: apply (H (fun v => @i_atom Σf1 Σp1 _ _ (PredApp n) (d::v))).
4: now exists d. 3: intros [] ar'; cbn; destruct_eq_dec. all: easy.
+ intros [d H]. exists (fun v => @i_atom Σf1 Σp1 _ _ (PredApp n) (d::v)).
eexists. now exists d. eapply IHphi. 4: apply H. 3: intros [] ar'; cbn; destruct_eq_dec. all: easy.
+ intros [f [[d Hd] H]]. exists d. eapply IHphi. 4: apply H. 3: intros [] ar'; cbn; destruct_eq_dec. all: easy.
Qed.
Definition toSOLEnv rho1 :=
⟨ fun n => rho1 (initial_pos_i n),
fun _ ar v => rho1 0,
fun n ar v => i_atom (P:=PredApp ar) (rho1 (initial_pos_p n ar) :: v) ⟩.
Lemma toSOLEnv_henkin_env rho1 :
henkin_env funcs preds (toSOLEnv rho1).
Proof.
intros n ar. split. easy. now exists (rho1 (initial_pos_p n ar)).
Qed.
Lemma toFOLForm_correct_1To2' rho1 phi :
funcfree phi -> FOL.sat rho1 (toFOLForm' phi) <-> Henkin.sat funcs preds (toSOLEnv rho1) phi.
Proof.
intros F. apply toFOLForm_correct_1To2. apply F. reflexivity. reflexivity.
Qed.
Lemma constructed_henkin_model_comprehension rho1 :
(forall phi, toFOLTheory C phi -> FOL.sat rho1 phi) -> forall rho2, (forall x ar, preds ar (get_pred rho2 x ar)) -> forall n phi, funcfree phi -> Henkin.sat funcs preds rho2 (comprehension_form n phi).
Proof.
intros H rho2 Hrho2 n phi F. apply close_sat_funcfree with (rho := toSOLEnv rho1).
- apply comprehension_form_funcfree, F.
- intros x ar'. unfold preds. eexists. cbn. reflexivity.
- apply toFOLForm_correct_1To2'.
+ apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree, F.
+ apply H. eexists. split. reflexivity. now exists n, phi.
- apply Hrho2.
Qed.
Lemma constructed_henkin_interp_correct rho :
(forall x ar, preds ar (get_pred rho x ar)) -> (forall phi, C phi -> Henkin.sat funcs preds rho phi) -> henkin_interp I2 funcs preds.
Proof.
intros Hrho HC. split. easy.
intros P. unfold preds. assert (Henkin.sat funcs preds rho (close All (comprehension_form (ar_preds P) (atom (pred P) (tabulate (ar_preds P) var_indi))))) as H1.
{ apply HC. eexists. eexists. split. 2: reflexivity. now apply tabulate_Forall. }
eapply close_sat_funcfree with (sigma := rho) in H1.
- apply comprehension_form_correct in H1 as [P' [[d H1] H2]]. exists d.
intros v. specialize (H2 v). cbn in H2. rewrite Deduction.eval_tabulate in H2.
cbn. setoid_rewrite <- H2. setoid_rewrite H1. reflexivity.
- now apply comprehension_form_funcfree, tabulate_Forall.
- apply Hrho.
- apply Hrho.
Qed.
End FOModel_To_HenkinModel.
(** *** Full Translation of Validity *)
Notation "A ∪ B" := (fun x => A x \/ B x) (at level 30).
Definition validFO `{falsity_flag} (T : FOL.form -> Prop) phi :=
forall D (I : FOL.interp D) rho, (forall psi, T psi -> FOL.sat rho psi) -> FOL.sat rho phi.
Lemma henkin_valid_iff_firstorder_valid (T : SOL.form -> Prop) phi :
funcfree phi -> (forall psi, T psi -> funcfree psi) -> Henkin.validT T phi <-> validFO (toFOLTheory (T ∪ C)) (toFOLForm' phi).
Proof.
intros F TF. split.
- intros H D1 I1 rho1 HT. apply toFOLForm_correct_1To2'; trivial. apply H.
+ apply constructed_henkin_interp_correct with (rho := toSOLEnv _ rho1).
* intros x ar. unfold preds. eexists. cbn. reflexivity.
* intros psi' [? [? [? ->]]]. apply toFOLForm_correct_1To2'.
now apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree.
apply HT. eexists. split. reflexivity. right. eexists. eexists. split. 2: reflexivity. easy.
+ eapply constructed_henkin_model_comprehension.
intros psi' [? [->]]. apply HT. eexists. split. reflexivity. now right.
+ apply toSOLEnv_henkin_env.
+ intros psi H1. apply toFOLForm_correct_1To2'. now apply TF. apply HT. firstorder.
- intros H D2 I2 funcs preds HI HC rho2 H_rho2 HT.
unshelve eapply toFOLForm_correct_2To1'; trivial.
+ exact (get_indi rho2 0).
+ intros ar. exists (get_pred rho2 0 ar). apply H_rho2.
+ apply H. intros psi [phi' [-> [|[ar [phi'' [HF ->]]]]]].
* eapply toFOLForm_correct_2To1'. now apply TF. now apply HT.
* eapply toFOLForm_correct_2To1'. now apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree.
eapply close_sat_funcfree. now apply comprehension_form_funcfree.
intros x ar'. apply H_rho2. intros sigma H2. now apply HC.
Qed.
(** Completeness of derived deduction system *)
Section DerivedCompleteness.
Existing Instance FOL.falsity_on.
Notation "T ⊩1 phi" := (FOL.tprv T phi) (at level 61).
Definition tprv2_derived A phi := toFOLTheory (A ∪ C) ⊩1 toFOLForm' phi.
Notation "A ⊩2' phi" := (tprv2_derived A phi) (at level 61).
Hypothesis tprv1_sound : forall (T : FOL.form -> Prop) phi, T ⊩1 phi -> validFO T phi.
Hypothesis tprv1_complete : forall T phi, validFO T phi -> T ⊩1 phi.
Hypothesis Σp2_enumerable : enumerable__T Σp2.
Hypothesis Σf2_enumerable : enumerable__T Σf2.
Hypothesis Σp2_eq_dec : eq_dec Σp2.
Hypothesis Σf2_eq_dec : eq_dec Σf2.
Hypothesis tprv1_enumerable : enumerable__T Σf1 -> enumerable__T Σp1 -> forall T, enumerable T -> enumerable (FOL.tprv T).
Lemma tprv2_derived_sound (T : SOL.form -> Prop) phi :
funcfree phi -> (forall psi, T psi -> funcfree psi) -> T ⊩2' phi -> Henkin.validT T phi.
Proof.
intros ? ? H. now apply henkin_valid_iff_firstorder_valid, tprv1_sound, H.
Qed.
Lemma tprv2_derived_complete (T : SOL.form -> Prop) phi :
funcfree phi -> (forall psi, T psi -> funcfree psi) -> Henkin.validT T phi -> T ⊩2' phi.
Proof.
intros ? ? H. now apply tprv1_complete, henkin_valid_iff_firstorder_valid, H.
Qed.
Lemma tprv2_derived_enumerable (T : SOL.form -> Prop) :
enumerable T -> enumerable (tprv2_derived T).
Proof.
intros H. unfold tprv2_derived. apply enumerable_comp.
- apply tprv1_enumerable, toFOLTheory_enumerable, enumerable_disj.
now apply Sigma_f1_enumerable. now apply Sigma_p1_enumerable.
apply H. now apply C_enumerable.
- apply form_enumerable; trivial. apply enumT_binop. apply enumT_quantop.
- apply FOL.dec_form. now apply Sigma_f1_eq_dec. now apply Sigma_p1_eq_dec.
all: intros x y; unfold dec; decide equality.
Qed.
End DerivedCompleteness.
(** ** Deductive Reduction *)
(** *** Preliminaries *)
Section ArityBoundedSubst.
Context {Σf2' : SOL.funcs_signature}.
Context {Σp2' : SOL.preds_signature}.
Definition subst_all_below_ar_p (sigma : nat -> forall ar, predicate ar) ar :=
fun n ar' => if Compare_dec.lt_dec ar' ar then sigma n ar' else var_pred n.
Definition subst_all_from_ar_p (sigma : nat -> forall ar, predicate ar) ar :=
fun n ar' => if Compare_dec.lt_dec ar' ar then var_pred n else sigma n ar'.
Lemma subst_all_below_ar_bounded b phi sigma :
arity_bounded_p b phi -> phi[subst_all_below_ar_p sigma b]p = phi[sigma]p.
Proof.
intros B. eapply subst_ext_p_arity_bounded. apply B.
intros x ar H. unfold subst_all_below_ar_p.
now destruct Compare_dec.lt_dec; try lia.
Qed.
Lemma subst_all_from_ar_bounded b phi sigma :
arity_bounded_p b phi -> phi[subst_all_from_ar_p sigma b]p = phi.
Proof.
intros B. erewrite <- subst_id_p. eapply subst_ext_p_arity_bounded. apply B.
intros x ar H. unfold subst_all_from_ar_p.
now destruct Compare_dec.lt_dec; try lia.
Qed.
End ArityBoundedSubst.
(** Closing operation for predicate variables *)
Section ClosePredicateAr.
Context {Σf2' : SOL.funcs_signature}.
Context {Σp2' : SOL.preds_signature}.
Fixpoint close_p op phi n := match n with 0 => phi | S n => SOL.quant_pred op n (close_p op phi n) end.
Lemma close_p_subst_i op phi sigma n :
(close_p op phi n)[sigma]i = close_p op (phi[sigma]i) n.
Proof.
revert sigma. induction n; intros sigma; cbn. reflexivity. now rewrite IHn.
Qed.
Lemma close_p_subst_f op phi sigma n :
(close_p op phi n)[sigma]f = close_p op (phi[sigma]f) n.
Proof.
revert sigma. induction n; intros sigma; cbn. reflexivity. now rewrite IHn.
Qed.
Definition all_up_p sigma : nat -> forall ar, predicate ar :=
fun n ar => match n with 0 => var_pred 0 | S n => (sigma n ar)[↑ ar]p end.
Lemma close_p_subst_p op phi sigma n :
(close_p op phi n)[sigma]p = close_p op (phi[subst_all_below_ar_p (all_up_p sigma) n]p[subst_all_from_ar_p sigma n]p) n.
Proof.
rewrite subst_comp_p. revert sigma. induction n; intros sigma.
- apply subst_ext_p. intros n ar. unfold subst_all_below_ar_p, subst_all_from_ar_p.
now destruct Compare_dec.lt_dec; try lia.
- cbn. f_equal. rewrite IHn. f_equal. apply subst_ext_p. intros [] ar;
unfold subst_all_from_ar_p, subst_all_below_ar_p;
repeat (destruct Compare_dec.lt_dec, Compare_dec.lt_dec; try lia; try reflexivity; cbn).
all: unfold up_p, scons, scons_pred, scons_ar, shift, shift_p;
repeat (destruct PeanoNat.Nat.eq_dec as [->|]; try lia; try easy; cbn).
+ destruct sigma; cbn; try easy. now destruct PeanoNat.Nat.eq_dec as [->|]; try lia.
+ destruct n0; repeat (destruct PeanoNat.Nat.eq_dec as [->|]; try lia; try easy; cbn);
destruct sigma; cbn; try reflexivity; repeat (try rewrite nat_eq_dec_same;
try destruct PeanoNat.Nat.eq_dec as [->|]; try destruct Compare_dec.lt_dec; try lia; try reflexivity; cbn).
+ destruct Compare_dec.lt_dec; try lia. destruct sigma; cbn; try easy. rewrite nat_eq_dec_same.
cbn. now destruct Compare_dec.lt_dec.
+ destruct sigma; cbn; try reflexivity. now destruct PeanoNat.Nat.eq_dec; try lia.
Qed.
Lemma close_p_subst_p' op phi sigma n :
(close_p op phi n)[sigma]p = close_p op (phi[fun x ar => if Compare_dec.lt_dec ar n then match x with 0 => var_pred 0 ar | S x => (sigma x ar)[↑ ar]p end else sigma x ar]p) n.
Proof.
rewrite close_p_subst_p, subst_comp_p. f_equal. apply subst_ext_p.
intros [] ar; destruct Compare_dec.lt_dec; cbn; unfold subst_all_below_ar_p, subst_all_from_ar_p;
repeat (destruct Compare_dec.lt_dec; try lia; try reflexivity; cbn).
unfold shift, shift_p. destruct sigma; cbn; try reflexivity. rewrite nat_eq_dec_same; cbn.
now destruct Compare_dec.lt_dec.
Qed.
Lemma close_p_subst_p_bounded op b phi sigma :
(arity_bounded_p b phi) -> (close_p op phi b)[sigma]p = close_p op (phi[all_up_p sigma]p) b.
Proof.
intros B. rewrite close_p_subst_p. f_equal. rewrite subst_all_from_ar_bounded.
apply subst_all_below_ar_bounded. apply B. apply arity_bounded_p_subst_p, B.
Qed.
Lemma close_p_bounded_indi n b op phi :
bounded_indi b phi -> bounded_indi b (close_p op phi n).
Proof.
now induction n.
Qed.
Lemma close_p_bounded_pred m ar b op phi :
bounded_pred ar b phi -> bounded_pred ar b (close_p op phi m).
Proof.
revert b. induction m; intros b H; cbn.
- exact H.
- destruct (PeanoNat.Nat.eq_dec ar m).
+ left. split. easy. apply IHm. eapply bounded_pred_up. 2: apply H. lia.
+ right. split. easy. now apply IHm.
Qed.
Lemma close_p_bounded_pred_2 m ar b op phi :
ar < m -> bounded_pred ar (S b) phi -> bounded_pred ar b (close_p op phi m).
Proof.
revert b. induction m; intros b H1 H2; cbn.
- lia.
- destruct (PeanoNat.Nat.eq_dec ar m).
+ left. split. easy. apply close_p_bounded_pred, H2.
+ right. split. easy. apply IHm. lia. apply H2.
Qed.
Lemma close_p_arity_bounded ar phi op n :
arity_bounded_p ar phi -> arity_bounded_p ar (close_p op phi n).
Proof.
now induction n.
Qed.
Lemma close_p_find_arity_bound_p op phi n :
find_arity_bound_p (close_p op phi n) = find_arity_bound_p phi.
Proof.
now induction n.
Qed.
(* Deduction *)
Definition shift_p_all : nat -> forall ar, predicate ar := fun n ar => var_pred (S n).
Definition subst_first_p_all (P : forall ar, predicate ar) : nat -> forall ar, predicate ar :=
fun n ar => match n with 0 => P ar | S n => var_pred n end.
Notation "⇑" := shift_p_all.
Notation "P ,," := (subst_first_p_all P) (at level 4, format "P ,,").
Lemma close_p_AllI {p' : peirce} A phi n :
List.map (subst_p (subst_all_below_ar_p ⇑ n)) A ⊢2 phi -> A ⊢2 close_p All phi n.
Proof.
revert A. induction n; intros A H; cbn.
- enough (List.map (subst_p (subst_all_below_ar_p ⇑ 0)) A = A) as <- by apply H.
clear H. induction A as [|psi A IH]; cbn. reflexivity. f_equal. rewrite <- subst_id_p.
now apply subst_ext_p. apply IH.
- apply AllI_p. apply IHn. rewrite List.map_map.
enough (List.map (subst_form_p (↑ n) >> subst_p (subst_all_below_ar_p ⇑ n)) A = List.map (subst_p (subst_all_below_ar_p ⇑ (S n))) A) as -> by apply H.
apply List.map_ext. intros psi. change (subst_form_p (↑ n) psi) with (psi[↑ n]p).
rewrite subst_comp_p. apply subst_ext_p. intros n' ar. unfold subst_all_below_ar_p, shift, shift_p.
now destruct Compare_dec.lt_dec, PeanoNat.Nat.eq_dec; cbn; destruct Compare_dec.lt_dec; try lia.
Qed.
Lemma close_p_AllI_nameless' {p' : peirce} phi A b n :
arity_bounded_p n phi
-> (forall ar, ar < n -> bounded_pred_L ar b A)
-> (forall ar, ar < n -> bounded_pred ar b phi)
-> A ⊢2 phi[(@var_pred _ b),,]p
-> A ⊢2 close_p All phi n.
Proof.
intros B B1. erewrite <- subst_all_below_ar_bounded. 2: apply B. clear B.
revert phi. induction n; intros phi B2 H; cbn.
- enough (phi = phi[subst_all_below_ar_p (@var_pred _ b),, 0]p) as -> by apply H.
rewrite <- subst_id_p at 1. apply subst_ext_p. intros n ar'. unfold subst_all_below_ar_p.
now destruct Compare_dec.lt_dec; try lia.
- apply AllI_p, nameless_equiv_all_p' with (n0:=b). apply B1. lia. apply close_p_bounded_pred.
eapply bounded_pred_up. 2: apply B2. lia. lia. rewrite close_p_subst_p'. apply IHn.
+ intros ar H1 psi H2. apply B1. lia. exact H2.
+ intros ar H1. apply bounded_pred_subst_p. 2: apply B2; lia.
intros []; destruct Compare_dec.lt_dec; try easy. destruct n0; cbn;
unfold subst_all_below_ar_p, shift, shift_p;
now repeat (destruct PeanoNat.Nat.eq_dec; try lia; cbn).
+ rewrite subst_comp_p. erewrite subst_ext_p. apply H.
intros [] ar; cbn; unfold subst_all_below_ar_p, shift, shift_p;
repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [->|]; cbn; try lia; try reflexivity).
destruct n0; cbn; repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [|]; cbn; try lia; try reflexivity).
Qed.
Lemma close_p_AllI_nameless {p' : peirce} phi A n :
arity_bounded_p n phi -> { x | A ⊢2 phi[(@var_pred _ x),,]p -> A ⊢2 close_p All phi n }.
Proof.
intros B. enough { b | forall ar, ar < n -> bounded_pred_L ar b A /\ bounded_pred ar b phi } as [x H].
{ exists x. apply close_p_AllI_nameless'. apply B. apply H. apply H. }
clear B. induction n.
- exists 0. intros ar H; lia.
- destruct IHn as [b H]. destruct (find_bounded_pred_L n (List.cons phi A)) as [b' H3].
exists (max b b'). intros ar H1. assert (ar < n \/ ar = n) as [H2| ->] by lia.
+ split. intros psi' H4. all: eapply bounded_pred_up; [| apply H]; try lia; easy.
+ split. intros psi' H4. all: eapply bounded_pred_up; [| apply H3]; try lia; firstorder.
Qed.
Lemma close_p_AllE phi {p' : peirce} A n P :
arity_bounded_p n phi -> A ⊢2 close_p All phi n -> A ⊢2 phi[P,,]p.
Proof.
intros B. erewrite <- subst_all_below_ar_bounded. 2: apply B.
clear B. induction n in phi |-*; cbn; intros H.
- erewrite subst_ext_p, subst_id_p. apply H. reflexivity.
- apply AllE_p with (P0 := P n) in H. rewrite close_p_subst_p' in H.
apply IHn in H. rewrite subst_comp_p in H. erewrite subst_ext_p. apply H.
intros [] ar; cbn; unfold subst_all_below_ar_p;
repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [->|]; try lia; try reflexivity; cbn);
destruct P; try reflexivity; cbn;
destruct n0; cbn; unfold shift, shift_p; repeat (try destruct Compare_dec.lt_dec;
try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn).
Qed.
Lemma close_p_ExE_nameless' {p' : peirce} phi psi A b n :
(forall ar, ar < n -> bounded_pred_L ar b A)
-> (forall ar, ar < n -> bounded_pred ar b phi)
-> (forall ar, ar < n -> bounded_pred ar b psi)
-> A ⊢2 close_p Ex phi n
-> phi[subst_all_below_ar_p (@var_pred _ b),, n]p :: A ⊢2 psi
-> A ⊢2 psi.
Proof.
induction n in A, phi |-*; intros B1 B2 B3 H1 H2; cbn in *.
- eapply IE. apply II, H2. enough (phi = phi[subst_all_below_ar_p (@var_pred _ b),, 0]p) as <- by apply H1.
rewrite <- subst_id_p at 1. apply subst_ext_p. intros n ar'. unfold subst_all_below_ar_p.
now destruct Compare_dec.lt_dec; try lia.
- eapply ExE_p. apply H1. eapply nameless_equiv_ex_p' with (n0:=b).
+ apply B1. lia.
+ apply B3. lia.
+ eapply bounded_pred_up. 2: apply close_p_bounded_pred, B2. lia. lia.
+ eapply IHn. 4: rewrite <- close_p_subst_p' with (sigma := (var_pred b n)..).
* intros ar H phi' [<-|]. apply bounded_pred_subst_p.
now intros []; cbn; destruct PeanoNat.Nat.eq_dec; try lia.
apply close_p_bounded_pred, B2. lia. apply B1. lia. easy.
* intros ar H. apply bounded_pred_subst_p. intros []; destruct Compare_dec.lt_dec; try lia.
reflexivity. now destruct n0; cbn; destruct PeanoNat.Nat.eq_dec; try lia; unfold shift, shift_p; cbn;
destruct PeanoNat.Nat.eq_dec; try lia. apply B2. lia.
* intros. apply B3. lia.
* apply Ctx. now left.
* rewrite subst_comp_p. erewrite subst_ext_p with (tau := subst_all_below_ar_p (@var_pred _ b),, (S n)).
eapply Weak. 2: apply H2. clear -H2; firstorder.
intros [|] ar; unfold subst_all_below_ar_p, shift, shift_p; destruct Compare_dec.lt_dec; cbn;
repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [->|]; try lia; try reflexivity; cbn).
destruct n0; cbn; repeat (destruct PeanoNat.Nat.eq_dec; try lia; cbn);
now destruct Compare_dec.lt_dec; try lia.
Qed.
Lemma close_p_ExE_nameless {p' : peirce} phi psi A n :
arity_bounded_p n phi -> A ⊢2 close_p Ex phi n -> { x | phi[(@var_pred _ x),,]p :: A ⊢2 psi -> A ⊢2 psi }.
Proof.
intros B. enough { b | (forall ar, ar < n -> (forall phi, List.In phi A -> bounded_pred ar b phi) /\ bounded_pred ar b phi /\ bounded_pred ar b psi) } as [x H].
{ exists x. erewrite <- subst_all_below_ar_bounded. 2: apply B. apply close_p_ExE_nameless'; firstorder. }
clear B. induction n.
- exists 0. intros ar H; lia.
- destruct IHn as [b H]. destruct (find_bounded_pred_L n (List.cons phi (List.cons psi A))) as [b' H3].
exists (max b b'). intros ar H1. assert (ar < n \/ ar = n) as [H2| ->] by lia.
+ repeat split. intros psi' H4. all: eapply bounded_pred_up; [| apply H]; try lia; easy.
+ repeat split. intros psi' H4. all: eapply bounded_pred_up; [| apply H3]; try lia; firstorder.
Qed.
Lemma close_p_ExI {p' : peirce} A phi n P :
arity_bounded_p n phi -> A ⊢2 phi[P,,]p -> A ⊢2 close_p Ex phi n.
Proof.
intros B. erewrite <- subst_all_below_ar_bounded. 2: apply B.
clear B. induction n in phi |-*; cbn; intros H.
- erewrite <- subst_id_p, subst_ext_p. apply H. intros n ar. unfold subst_all_below_ar_p.
now destruct Compare_dec.lt_dec; try lia.
- apply ExI_p with (P0:=P n). rewrite close_p_subst_p'. apply IHn.
erewrite subst_comp_p, subst_ext_p. apply H.
intros [] ar; cbn; unfold subst_all_below_ar_p;
repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [->|]; try lia; try reflexivity; cbn);
destruct P; cbn; try reflexivity. now destruct Compare_dec.lt_dec.
all: destruct n0; cbn; unfold shift, shift_p; repeat (try destruct Compare_dec.lt_dec;
try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn).
Qed.
End ClosePredicateAr.
Notation "⇑" := shift_p_all.
Notation "P ,," := (subst_first_p_all P) (at level 4, format "P ,,").
(** Add falsity symbol to signature *)
Inductive ExtendedPreds :=
| OldPred : SOL.preds -> ExtendedPreds
| FalsePred : nat -> ExtendedPreds.
Instance Σp2' : SOL.preds_signature := {|
SOL.preds := ExtendedPreds ;
SOL.ar_preds P := match P with OldPred P => SOL.ar_preds P | FalsePred ar => ar end
|}.
(** *** Removal of Falsity Symbols *)
Fixpoint removeFalsePred (phi : @SOL.form Σf2 Σp2' _) : @SOL.form Σf2 Σp2 _ := match phi with
| SOL.atom (pred (OldPred p)) v => SOL.atom (pred p) v
| SOL.atom (pred (FalsePred ar)) v => SOL.fal
| SOL.atom (var_pred x ar) v => SOL.atom (var_pred x ar) v
| SOL.fal => SOL.fal
| SOL.bin op phi psi => SOL.bin op (removeFalsePred phi) (removeFalsePred psi)
| SOL.quant_indi op phi => SOL.quant_indi op (removeFalsePred phi)
| SOL.quant_func op ar phi => SOL.quant_func op ar (removeFalsePred phi)
| SOL.quant_pred op ar phi => SOL.quant_pred op ar (removeFalsePred phi)
end.
Lemma removeFalsePred_subst_i phi sigma :
(removeFalsePred phi)[sigma]i = removeFalsePred (phi[sigma]i).
Proof.
induction phi in sigma |- *; cbn; try congruence. now destruct p as [|[]].
Qed.
Lemma removeFalsePred_subst_f phi sigma :
(removeFalsePred phi)[sigma]f = removeFalsePred (phi[sigma]f).
Proof.
induction phi in sigma |- *; cbn; try congruence. now destruct p as [|[]].
Qed.
Lemma removeFalsePred_subst_p phi sigma sigma' :
(forall n ar, (exists x, sigma n ar = var_pred x /\ sigma' n ar = var_pred x)
\/ exists P (e : ar_preds P = ar), sigma n ar = Util.cast _ e (pred P) /\ sigma' n ar = Util.cast _ e (pred (OldPred P)))
-> (removeFalsePred phi)[sigma]p = removeFalsePred (phi[sigma']p).
Proof.
induction phi in sigma, sigma' |- *; cbn; intros H.
- reflexivity.
- destruct p as [|[]]; cbn; try reflexivity. now destruct (H n ar) as [[x [-> ->]]|[P [<- [-> ->]]]].
- erewrite IHphi1, IHphi2. reflexivity. apply H. apply H.
- erewrite IHphi. reflexivity. apply H.
- erewrite IHphi. reflexivity. apply H.
- erewrite IHphi. reflexivity. intros [] ar; cbn.
+ destruct PeanoNat.Nat.eq_dec as [->|]. left. now exists 0. edestruct H as [[x [-> ->]]|[P [<- [-> ->]]]].
* left. exists x; cbn. unfold shift, shift_p. now destruct PeanoNat.Nat.eq_dec.
* right. now exists P, eq_refl.
+ destruct PeanoNat.Nat.eq_dec as [->|]; edestruct H as [[x [-> ->]]|[P [<- [-> ->]]]].
* left. exists (S x). cbn; unfold shift, shift_p; now destruct PeanoNat.Nat.eq_dec.
* right. now exists P, eq_refl.
* left. exists x. cbn; unfold shift, shift_p; now destruct PeanoNat.Nat.eq_dec.
* right. now exists P, eq_refl.
Qed.
Lemma removeFalsePred_forall_n n phi :
removeFalsePred (forall_n n phi) = forall_n n (removeFalsePred phi).
Proof.
induction n; cbn; congruence.
Qed.
Lemma removeFalsePred_close_p op phi n :
removeFalsePred (close_p op phi n) = close_p op (removeFalsePred phi) n.
Proof.
induction n; cbn. reflexivity. now rewrite IHn.
Qed.
Lemma removeFalsePred_arity_bounded_p phi n :
arity_bounded_p n phi <-> arity_bounded_p n (removeFalsePred phi).
Proof.
induction phi. 2: now destruct p as [|[]]. all: firstorder.
Qed.
Lemma removeFalsePred_funcfree phi :
funcfree phi -> funcfree (removeFalsePred phi).
Proof.
intros F. induction phi; cbn; firstorder. now destruct p as [|[]]; cbn.
Qed.
Lemma replace_FalsePred_subst {p' : peirce} (phi : @SOL.form Σf2 Σp2' _) ar n :
List.nil ⊢2 (forall_n ar (p$n (tabulate ar var_indi) <--> ⊥)) --> (removeFalsePred phi[(@pred Σp2' (FalsePred ar))..]p <--> (removeFalsePred phi)[(var_pred n ar)..]p).
Proof.
enough (forall sigma1 sigma2 n m,
sigma1 m ar = pred (FalsePred ar)
-> sigma2 m ar = var_pred n ar
-> (forall x ar', x <> m \/ ar' <> ar -> exists y, sigma1 x ar' = var_pred y /\ sigma2 x ar' = var_pred y)
-> List.nil ⊢2 (forall_n ar (p$n (tabulate ar var_indi) <--> ⊥)) --> (removeFalsePred phi[sigma1]p <--> (removeFalsePred phi)[sigma2]p)) as X.
{ apply X with (m:=0); cbn -[PeanoNat.Nat.eq_dec].
- now rewrite nat_eq_dec_same.
- now rewrite nat_eq_dec_same.
- intros x ar' [].
+ destruct x; try lia; cbn. destruct PeanoNat.Nat.eq_dec as [->|]; now eexists.
+ exists x. destruct x; cbn; now destruct PeanoNat.Nat.eq_dec as [->|]. }
induction phi; cbn; intros sigma1 sigma2 n' m H1 H2 H3; apply II.
- apply CI; apply II; apply Ctx; now left.
- destruct p as [|[]]; cbn. 2,3: apply CI; apply II; apply Ctx; now left.
specialize (H3 n0 ar0). destruct (PeanoNat.Nat.eq_dec n0 m) as [->|].