-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPA.v
1974 lines (1681 loc) · 88.3 KB
/
PA.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
(** * Second-Order Peano Arithmetic *)
Require Import SOL.
Require Import FullSyntax.
Require Import Subst.
Require Import Tarski.
Require Import Vector.
Import VectorNotations.
Require Import VectorLib.
Require Import Decidable Enumerable.
Require Import Util.
Import SubstNotations.
Require Import Equations.Equations Equations.Prop.DepElim.
Derive Signature for Vector.t.
Derive Signature for function.
Derive Signature for predicate.
Require Import Lia.
Require Import PeanoNat.
Inductive PA_funcs : Type := Zero | Succ | Plus | Mult.
Definition PA_funcs_ar (f : PA_funcs ) :=
match f with
| Zero => 0
| Succ => 1
| Plus => 2
| Mult => 2
end.
Inductive PA_preds : Type := Eq : PA_preds.
Definition PA_preds_ar (P : PA_preds) := match P with Eq => 2 end.
Instance PA_funcs_signature : funcs_signature :=
{| syms := PA_funcs ; ar_syms := PA_funcs_ar |}.
Instance PA_preds_signature : preds_signature :=
{| preds := PA_preds ; ar_preds := PA_preds_ar |}.
Arguments Vector.cons {_} _ {_} _, _ _ _ _.
Definition zero := func (sym Zero) ([]).
Notation "'σ' x" := (func (sym Succ) ([x])) (at level 37).
Notation "x '⊕' y" := (func (sym Plus) ([x ; y])) (at level 39).
Notation "x '⊗' y" := (func (sym Mult) ([x ; y])) (at level 38).
Notation "x '==' y" := (atom (pred Eq) ([x ; y])) (at level 40).
(** With concrete instances for functions and predicates
we get a real equality decider. *)
Instance PA_funcs_signature_eq_dec :
Decidable.eq_dec PA_funcs_signature.
Proof.
intros x y. unfold dec. decide equality.
Qed.
Instance PA_preds_signature_eq_dec :
Decidable.eq_dec PA_preds_signature.
Proof.
intros [] []. now left.
Qed.
Definition L_PA_funcs (n : nat) := List.cons Zero (List.cons Succ (List.cons Plus (List.cons Mult List.nil))).
Definition L_PA_preds (n : nat) := List.cons Eq List.nil.
Instance PA_funcs_enum :
list_enumerator__T L_PA_funcs PA_funcs.
Proof.
intros []; exists 0; firstorder.
Qed.
Instance PA_preds_enum :
list_enumerator__T L_PA_preds PA_preds.
Proof.
intros []; exists 0; firstorder.
Qed.
Lemma PA_form_enumerable :
enumerable__T form.
Proof.
apply form_enumerable.
- apply list_enumerable__T_enumerable. exists L_PA_funcs. apply PA_funcs_enum.
- apply list_enumerable__T_enumerable. exists L_PA_preds. apply PA_preds_enum.
- apply enumT_binop.
- apply enumT_quantop.
Qed.
(** ** Axioms *)
Section Model.
Definition ax_eq_refl := ∀i $0 == $0.
Definition ax_eq_symm := ∀i ∀i $1 == $0 --> $0 == $1.
Definition ax_eq_trans := ∀i ∀i ∀i $2 == $1 --> $1 == $0 --> $2 == $0.
Definition ax_zero_succ := ∀i zero == σ $0 --> fal.
Definition ax_succ_inj := ∀i ∀i σ $1 == σ $0 --> $1 == $0.
Definition ax_add_zero := ∀i zero ⊕ $0 == $0.
Definition ax_add_rec := ∀i ∀i (σ $0) ⊕ $1 == σ ($0 ⊕ $1).
Definition ax_mul_zero := ∀i zero ⊗ $0 == zero.
Definition ax_mul_rec := ∀i ∀i σ $1 ⊗ $0 == $0 ⊕ $1 ⊗ $0.
Definition ax_ind := ∀p(1) p$0 ([zero]) --> (∀i p$0 ([$0]) --> p$0 ([σ $0])) --> ∀i p$0 ([$0]).
Import List ListNotations.
Definition PA_L := [ ax_eq_refl ; ax_eq_symm ; ax_zero_succ ; ax_succ_inj ; ax_add_zero ; ax_add_rec ; ax_mul_zero ; ax_mul_rec ; ax_ind ].
Definition PA phi := In phi PA_L.
Import VectorNotations.
Lemma PA_enumerable :
enumerable PA.
Proof.
exists (fun n => nth n (map Some PA_L) None). intros phi. split.
- intros H. repeat destruct H as [<-|H].
now exists 0. now exists 1. now exists 2. now exists 3. now exists 4.
now exists 5. now exists 6. now exists 7. now exists 8. easy.
- intros [n H]. assert (forall x y : form, Some x = Some y -> x = y) as Some_inj by congruence.
do 9 try destruct n as [|n]; try apply Some_inj in H as <-. 1-9: firstorder.
destruct n; cbn in H; congruence.
Qed.
Definition empty_PA_env M : env (M_domain M) := ⟨ fun n => i_f (M_domain M) Zero ([]) , fun n ar v => i_f (M_domain M) Zero ([]), fun n ar v => True ⟩.
Variable PA_M : Model_of PA.
Notation "'izero'" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Zero ([])).
Notation "'iσ' x" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Succ ([x])) (at level 37).
Notation "x 'i⊕' y" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Plus ([x ; y])) (at level 39).
Notation "x 'i⊗' y" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Mult ([x ; y])) (at level 38).
Notation "x 'i==' y" := (@i_P _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Eq ([x ; y])) (at level 40).
Lemma eq_reflexive x :
x i== x.
Proof. revert x. apply (M_correct PA_M ax_eq_refl ltac:(firstorder) (empty_PA_env _)). Qed.
Lemma eq_symm x y :
x i== y -> y i== x.
Proof. apply (M_correct PA_M ax_eq_symm ltac:(firstorder) (empty_PA_env _)). Qed.
Lemma zero_succ' x :
izero i== iσ x -> False.
Proof. apply (M_correct PA_M ax_zero_succ ltac:(firstorder) (empty_PA_env _)). Qed.
Lemma succ_inj' x y :
iσ x i== iσ y -> x i== y.
Proof. apply (M_correct PA_M ax_succ_inj ltac:(firstorder) (empty_PA_env _)). Qed.
(** Simplify induction axiom by removing the vector *)
Lemma induction (P : M_domain PA_M -> Prop) :
P izero -> (forall x, P x -> P (iσ x)) -> forall x, P x.
Proof.
pose (P' := fun v : vec _ 1 => P (Vector.hd v)).
change (P' ([izero]) -> (forall x, P' ([x]) -> P' ([iσ x])) -> forall x, P' ([x])).
apply (M_correct PA_M ax_ind ltac:(firstorder) (empty_PA_env _)).
Qed.
Lemma case_analysis x :
x = izero \/ exists x', x = iσ x'.
Proof.
revert x. apply induction.
- now left.
- intros x _. right. now exists x.
Qed.
Lemma eq_sem x y :
x i== y <-> x = y.
Proof.
split.
- revert x y. apply (induction (fun x => forall y, x i== y -> x = y)).
+ intros y H. destruct (case_analysis y) as [->|[y' ->]].
* reflexivity.
* now apply zero_succ' in H.
+ intros x IH y H. destruct (case_analysis y) as [->|[y' ->]].
* now apply eq_symm, zero_succ' in H.
* rewrite (IH y'). reflexivity. now apply succ_inj'.
- intros ->. apply eq_reflexive.
Qed.
Lemma zero_succ x :
izero = iσ x -> False.
Proof. intros H%eq_sem. now apply (zero_succ' x). Qed.
Lemma succ_inj x y :
iσ x = iσ y -> x = y.
Proof. intros H%eq_sem. now apply eq_sem, (succ_inj' x y). Qed.
Lemma add_zero x :
izero i⊕ x = x.
Proof. apply eq_sem, (M_correct PA_M ax_add_zero ltac:(firstorder) (empty_PA_env _)). Qed.
Lemma add_rec x y :
iσ x i⊕ y = iσ (x i⊕ y).
Proof. apply eq_sem, (M_correct PA_M ax_add_rec ltac:(firstorder) (empty_PA_env _)). Qed.
Lemma mul_zero x :
izero i⊗ x = izero.
Proof. apply eq_sem, (M_correct PA_M ax_mul_zero ltac:(firstorder) (empty_PA_env _)). Qed.
Lemma mul_rec x y :
iσ x i⊗ y = y i⊕ (x i⊗ y).
Proof. apply eq_sem, (M_correct PA_M ax_mul_rec ltac:(firstorder) (empty_PA_env _)). Qed.
(** Convert from nat to this model *)
Fixpoint to_domain n : M_domain PA_M := match n with
| 0 => izero
| S n => iσ (to_domain n)
end.
Lemma to_domain_add x y :
to_domain (x + y) = to_domain x i⊕ to_domain y.
Proof.
revert y. induction x; intros; cbn.
- symmetry. apply add_zero.
- rewrite add_rec. now repeat f_equal.
Qed.
Lemma to_domain_mul x y :
to_domain (x * y) = to_domain x i⊗ to_domain y.
Proof.
revert y. induction x; intros; cbn.
- symmetry. apply mul_zero.
- rewrite mul_rec. rewrite to_domain_add. now repeat f_equal.
Qed.
Lemma to_domain_injective x x' :
to_domain x = to_domain x' -> x = x'.
Proof.
revert x'. induction x; destruct x'.
- reflexivity.
- now intros H%zero_succ.
- intros H. symmetry in H. now apply zero_succ in H.
- intros H%succ_inj. now rewrite (IHx x').
Qed.
End Model.
(** ** Standard Model *)
Section StandardModel.
Definition std_interp_f (f : syms) : vec nat (ar_syms f) -> nat :=
match f with
| Zero => fun _ => 0
| Succ => fun v => S (Vector.hd v)
| Plus => fun v => Vector.hd v + Vector.hd (Vector.tl v)
| Mult => fun v => Vector.hd v * Vector.hd (Vector.tl v)
end.
Definition std_interp_P (P : preds) : vec nat (ar_preds P) -> Prop :=
match P with
| Eq => fun v => Vector.hd v = Vector.hd (Vector.tl v)
end.
Instance I_nat : interp nat := {| i_f := std_interp_f ; i_P := std_interp_P |}.
Definition Standard_Model : Model := {|
M_domain := nat ;
M_interp := I_nat
|}.
(* Automatically turns into relational interpretation via coercion *)
Definition Standard_Model_p : Model_p := {|
M_p_domain := nat ;
M_p_interp := I_nat
|}.
Lemma std_model_correct :
forall phi, PA phi -> Standard_Model ⊨ phi.
Proof.
intros phi H. repeat try destruct H as [<-|H]; hnf; cbn; try congruence.
intros rho P H IH n. induction n; auto. easy.
Qed.
Lemma std_model_p_correct :
forall phi, PA phi -> Standard_Model_p ⊨p phi.
Proof.
intros phi H rho. repeat destruct H as [<-|H]; cbn.
- intros d. now exists [d;d].
- intros ? ? [v [[-> [-> _]] ?]]. repeat depelim v. now exists [h0;h].
- intros d [v [[[] [[v' [[]]] []]]]]. repeat depelim v. repeat depelim v'. lia.
- intros ? ? [v1 [[[v2 [[->]]] [[v3 [[->] ]] ?]] ?]]. repeat depelim v1. repeat depelim v2. repeat depelim v3.
cbn in *. exists [h1;h2]. cbn. split. easy. lia.
- intros d. exists [d;d]. repeat split; cbn. exists [0;d]. repeat split; trivial. exact [].
- intros d1 d2. exists [S d2 + d1; S (d2 + d1)]. repeat split.
+ exists [S d2;d1]. repeat split. now exists [d2].
+ exists [d2 + d1]. repeat split. now exists [d2;d1].
- intros d. exists [0;0]. repeat split. 2: exact []. exists [0;d]. repeat split. exact [].
- intros d1 d2. exists [S d1 * d2; d2 + (d1 * d2)]. repeat split.
+ exists [S d1;d2]. repeat split. now exists [d1].
+ exists [d2;d1 * d2]. repeat split. now exists [d1;d2].
- intros P [v1 [[[_ [_ H1]] _] H2]] H3 d. repeat depelim v1; cbn in *.
rewrite <- H1 in H2. induction d as [|d [v2 [[-> _] IH]]].
+ now exists [0].
+ repeat depelim v2. exists [S h0]. repeat split. destruct (H3 h0) as [v3 [[[v4 [[-> _] ?]] ?] ?]]. now exists [h0].
repeat depelim v3. repeat depelim v4. cbn in *. congruence.
- now exfalso.
Qed.
Definition Standard_PA_Model : Model_of PA := {|
M_model := Standard_Model ;
M_correct := std_model_correct ;
|}.
Definition Standard_PA_Model_p : Model_p_of PA := {|
M_p_model := Standard_Model_p ;
M_p_correct := std_model_p_correct ;
|}.
End StandardModel.
(** ** Signature Embedding *)
(** We can embed the PA signature into the formula and translate to
an arbitrary signature. *)
Section EmbedSignature.
Definition Σf := PA_funcs_signature.
Definition Σp := PA_preds_signature.
Context {Σf' : funcs_signature}.
Context {Σp' : preds_signature}.
Context {D : Type}.
Context {I : @interp Σf Σp D}.
Context {I' : @interp Σf' Σp' D}.
(* We assume that the PA functions and predicates are inside the
environment at
xO = Position of zero
xS = Position of succ
xA = Position of add
xA + 1 = Position of mul
Replace function and predicate symbols with the corresponding
variable and shift the existing variables.
*)
Fixpoint embed_term xO xS xA (t : @term Σf) : @term Σf' := match t with
| var_indi x => var_indi x
| func (sym Zero) v => func (@var_func _ xO 0) (Vector.map (embed_term xO xS xA) v)
| func (sym Succ) v => func (@var_func _ xS 1) (Vector.map (embed_term xO xS xA) v)
| func (sym Plus) v => func (@var_func _ xA 2) (Vector.map (embed_term xO xS xA) v)
| func (sym Mult) v => func (@var_func _ (S xA) 2) (Vector.map (embed_term xO xS xA) v)
| func (@var_func _ x 0) v => if Compare_dec.le_lt_dec xO x then func (@var_func _ (S x) 0) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 0) (Vector.map (embed_term xO xS xA) v)
| func (@var_func _ x 1) v => if Compare_dec.le_lt_dec xS x then func (@var_func _ (S x) 1) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 1) (Vector.map (embed_term xO xS xA) v)
| func (@var_func _ x 2) v => if Compare_dec.le_lt_dec xA x then func (@var_func _ (S (S x)) 2) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 2) (Vector.map (embed_term xO xS xA) v)
| func (@var_func _ x ar) v => func (@var_func _ x ar) (Vector.map (embed_term xO xS xA) v)
end.
Fixpoint embed_form xO xS xA xEq (phi : @form Σf Σp _) : @form Σf' Σp' _ := match phi with
| fal => fal
| atom (pred Eq) v => atom (@var_pred _ xEq 2) (Vector.map (embed_term xO xS xA) v)
| atom (@var_pred _ x 2) v => if Compare_dec.le_lt_dec xEq x then atom (@var_pred _ (S x) 2) (Vector.map (embed_term xO xS xA) v) else atom (@var_pred _ x 2) (Vector.map (embed_term xO xS xA) v)
| atom (@var_pred _ x ar) v => atom (@var_pred _ x ar) (Vector.map (embed_term xO xS xA) v)
| bin op phi psi => bin op (embed_form xO xS xA xEq phi) (embed_form xO xS xA xEq psi)
| quant_indi op phi => quant_indi op (embed_form xO xS xA xEq phi)
| quant_func op 0 phi => quant_func op 0 (embed_form (S xO) xS xA xEq phi)
| quant_func op 1 phi => quant_func op 1 (embed_form xO (S xS) xA xEq phi)
| quant_func op 2 phi => quant_func op 2 (embed_form xO xS (S xA) xEq phi)
| quant_func op ar phi => quant_func op ar (embed_form xO xS xA xEq phi)
| quant_pred op 2 phi => quant_pred op 2 (embed_form xO xS xA (S xEq) phi)
| quant_pred op ar phi => quant_pred op ar (embed_form xO xS xA xEq phi)
end.
Definition pred n := match n with 0 => 0 | S n => n end.
(* Predicate that states that rho' contains the PA signature inserted at
positions xO, xS, xA and xEq, and matches up with rho. *)
Definition env_contains_PA (rho rho' : env D) xO xS xA xEq :=
(forall n, get_indi rho n = get_indi rho' n) /\
(forall n ar, get_func rho' n ar = match ar with
| 0 => match Compare_dec.lt_eq_lt_dec n xO with inleft (left _) => get_func rho n 0 | inleft (right _) => @i_f _ _ D I Zero | inright _ => get_func rho (pred n) 0 end
| 1 => match Compare_dec.lt_eq_lt_dec n xS with inleft (left _) => get_func rho n 1 | inleft (right _) => @i_f _ _ D I Succ | inright _ => get_func rho (pred n) 1 end
| 2 => if Nat.eq_dec n xA then @i_f _ _ D I Plus else match Compare_dec.lt_eq_lt_dec n (S xA) with inleft (left _) => get_func rho n 2 | inleft (right _) => @i_f _ _ D I Mult | inright _ => get_func rho (pred (pred n)) 2 end
| ar => get_func rho n ar
end) /\
(forall n ar, get_pred rho' n ar = match ar with
| 2 => match Compare_dec.lt_eq_lt_dec n xEq with inleft (left _) => get_pred rho n 2 | inleft (right _) => @i_P _ _ D I Eq | inright _ => get_pred rho (pred n) 2 end
| ar => get_pred rho n ar
end).
Local Arguments Nat.eq_dec : simpl never.
Local Arguments Compare_dec.lt_eq_lt_dec : simpl never.
Ltac solve_env E :=
try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
try destruct Nat.eq_dec; try lia; cbn; try rewrite E;
try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
try destruct Nat.eq_dec; try lia;
try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
try destruct Nat.eq_dec; try lia; cbn; try rewrite E;
try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
try destruct Nat.eq_dec; try lia.
Lemma env_contains_PA_scons_i rho rho' xO xS xA xEq d :
env_contains_PA rho rho' xO xS xA xEq -> env_contains_PA ⟨d .: get_indi rho, get_func rho, get_pred rho⟩ ⟨d .: get_indi rho', get_func rho', get_pred rho'⟩ xO xS xA xEq.
Proof.
intros E. split. 2: apply E. intros []. reflexivity. apply E.
Qed.
Lemma env_contains_PA_scons_f {rho rho' xO xS xA xEq ar} (f : vec D ar -> D) :
env_contains_PA rho rho' xO xS xA xEq ->
match ar with
| 0 => env_contains_PA ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ (S xO) xS xA xEq
| 1 => env_contains_PA ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO (S xS) xA xEq
| 2 => env_contains_PA ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO xS (S xA) xEq
| ar => env_contains_PA ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO xS xA xEq
end.
Proof.
intros E. unfold scons, scons_env_func, scons_ar. destruct ar as [|[|[]]];
split; try apply E; split; try apply E; destruct E as [_ [E2 _]];
intros [|[|[]]] [|[|[]]]; solve_env E2; reflexivity.
Qed.
Lemma env_contains_PA_scons_p {rho rho' xO xS xA xEq ar} (P : vec D ar -> Prop) :
env_contains_PA rho rho' xO xS xA xEq ->
match ar with
| 2 => env_contains_PA ⟨get_indi rho, get_func rho, P .: get_pred rho⟩ ⟨get_indi rho', get_func rho', P .: get_pred rho'⟩ xO xS xA (S xEq)
| _ => env_contains_PA ⟨get_indi rho, get_func rho, P .: get_pred rho⟩ ⟨get_indi rho', get_func rho', P .: get_pred rho'⟩ xO xS xA xEq
end.
Proof.
intros E. unfold scons, scons_env_func, scons_ar. destruct ar as [|[|[]]];
split; try apply E; split; try apply E; destruct E as [_ [_ E3]];
intros [|[|[]]] [|[|[]]]; solve_env E3; reflexivity.
Qed.
Lemma embed_term_correct rho rho' xO xS xA xEq t :
env_contains_PA rho rho' xO xS xA xEq -> @eval Σf Σp D I rho t = @eval Σf' Σp' D I' rho' (embed_term xO xS xA t).
Proof.
intros E. induction t; cbn.
- apply E.
- destruct E as [_ [E2 _]]. apply map_ext_forall in IH. destruct ar as [|[|[]]];
try destruct Compare_dec.le_lt_dec; cbn; rewrite E2;
try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
try destruct Nat.eq_dec; try lia; now rewrite map_map, IH.
- destruct E as [_ [E2 _]]. apply map_ext_forall in IH. destruct f; cbn in *;
rewrite E2; destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
try destruct Nat.eq_dec; try lia; now rewrite map_map, IH.
Qed.
Lemma embed_form_correct rho rho' xO xS xA xEq phi :
env_contains_PA rho rho' xO xS xA xEq -> @sat Σf Σp D I rho phi <-> @sat Σf' Σp' D I' rho' (embed_form xO xS xA xEq phi).
Proof.
revert rho rho' xO xS xA xEq. induction phi; intros rho rho' xO xS xA xEq E; cbn.
- reflexivity.
- assert (map (@eval Σf Σp D I rho) v = map (fun t => @eval Σf' Σp' D I' rho' (embed_term xO xS xA t)) v) as Hv'.
{ clear p. induction v. reflexivity. cbn; f_equal.
apply (embed_term_correct _ _ _ _ _ _ _ E). apply IHv. }
destruct E as [_ [_ E3]]. destruct p; cbn.
+ destruct ar as [|[|[]]];
try destruct Compare_dec.le_lt_dec; cbn; rewrite E3;
try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
now rewrite map_map, Hv'.
+ destruct P; cbn in *. rewrite E3.
destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia.
now rewrite map_map, Hv'.
- specialize (IHphi1 rho rho' xO xS xA xEq E);
specialize (IHphi2 rho rho' xO xS xA xEq E).
destruct b; tauto.
- destruct q.
+ split; intros H d; eapply IHphi. 2,4: apply (H d). all: now apply env_contains_PA_scons_i.
+ split; intros [d H]; exists d; eapply IHphi. 2,4: apply H. all: now apply env_contains_PA_scons_i.
- destruct q; destruct n as [|[|[]]]; split.
1-8: intros H f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA_scons_f f).
all: intros [f H]; exists f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA_scons_f f).
- destruct q; destruct n as [|[|[]]]; split.
1-8: intros H P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA_scons_p P).
all: intros [P H]; exists P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA_scons_p P).
Qed.
End EmbedSignature.
Section EmbedSignatureFuncfree.
Context {Σf' : funcs_signature}.
Context {Σp' : preds_signature}.
Context {D : Type}.
Context {I : @interp_p Σf Σp D}.
Context {I' : @interp Σf' Σp' D}.
Definition sshift k : nat -> term :=
fun n => match n with 0 => $0 | S n => $(1 + k + n) end.
Fixpoint embed_term_funcfree (t : @term Σf) : @form Σf' Σp' _ := match t with
| var_indi x => ∀p(1) atom (var_pred 0) ([var_indi 0]) --> atom (var_pred 0) ([var_indi (S x)])
| func (sym Zero) v => atom (var_pred 0) ([var_indi 0])
| func (sym Succ) v => let v' := Vector.map embed_term_funcfree v in
∃i (Vector.hd v')[sshift 1]i
∧ atom (var_pred 0) ([i$1 ; i$0])
| func (sym Plus) v => let v' := Vector.map embed_term_funcfree v in
∃i (Vector.hd v')[sshift 1]i
∧ ∃i (Vector.hd (Vector.tl v'))[sshift 2]i
∧ atom (var_pred 0) ([i$2 ; i$1 ; i$0])
| func (sym Mult) v => let v' := Vector.map embed_term_funcfree v in
∃i (Vector.hd v')[sshift 1]i
∧ ∃i (Vector.hd (Vector.tl v'))[sshift 2]i
∧ atom (var_pred 1) ([i$2 ; i$1 ; i$0])
| func (var_func _) _ => atom (var_pred 0) (Vector.nil _)
end.
Fixpoint embed_form_funcfree (phi : @form Σf Σp _) : @form Σf' Σp' _ := match phi with
| fal => fal
| atom (SOL.pred Eq) v => ∃i embed_term_funcfree (Vector.hd v)
∧ ∃i (embed_term_funcfree (Vector.hd (Vector.tl v)))[sshift 1]i
∧ atom (var_pred 1) ([i$1 ; i$0])
| atom (var_pred _) _ => atom (var_pred 0) (Vector.nil _)
| bin op phi psi => bin op (embed_form_funcfree phi) (embed_form_funcfree psi)
| quant_indi op phi => quant_indi op (embed_form_funcfree phi)
| quant_func op ar phi => quant_func op ar (embed_form_funcfree phi)
| quant_pred op ar phi => quant_pred op ar (embed_form_funcfree phi)
end.
Lemma embed_term_funcfree_funcfree t :
funcfree (embed_term_funcfree t).
Proof.
induction t; try easy. destruct f; repeat depelim v; cbn in *; repeat split;
apply funcfree_subst_i; try apply IH; now intros [].
Qed.
Lemma sat_sshift1' rho_i rho_f rho_p x y (phi : @form Σf' Σp' _) :
funcfree phi -> ⟨⟨y .: x .: rho_i, rho_f, rho_p⟩⟩ ⊨p phi[sshift 1]i <-> ⟨⟨y .: rho_i, rho_f, rho_p⟩⟩ ⊨p phi.
Proof.
intros F. setoid_rewrite sat_p_comp_i; trivial. erewrite sat_p_ext.
split; eauto. intros n. split. 2: easy. now destruct n. intros []; eexists; reflexivity.
Qed.
Lemma sat_sshift2' rho_i rho_f rho_p x y z (phi : @form Σf' Σp' _) :
funcfree phi -> ⟨⟨z .: y .: x .: rho_i, rho_f, rho_p⟩⟩ ⊨p phi[sshift 2]i <-> ⟨⟨z .: rho_i, rho_f, rho_p⟩⟩ ⊨p phi.
Proof.
intros F. setoid_rewrite sat_p_comp_i; trivial. erewrite sat_p_ext.
split; eauto. intros n. split. 2: easy. now destruct n. intros []; eexists; reflexivity.
Qed.
Lemma sat_sshift1 rho_i rho_f rho_p x y (phi : @form Σf' Σp' _) :
funcfree phi -> ⟨y .: x .: rho_i, rho_f, rho_p⟩ ⊨ phi[sshift 1]i <-> ⟨y .: rho_i, rho_f, rho_p⟩ ⊨ phi.
Proof.
intros F. setoid_rewrite sat_comp_i; trivial. erewrite sat_ext.
split; eauto. intros n. split. 2: easy. now destruct n.
Qed.
Lemma sat_sshift2 rho_i rho_f rho_p z x y (phi : @form Σf' Σp' _) :
funcfree phi -> ⟨z .: y .: x .: rho_i, rho_f, rho_p⟩ ⊨ phi[sshift 2]i <-> ⟨z .: rho_i, rho_f, rho_p⟩ ⊨ phi.
Proof.
intros F. setoid_rewrite sat_comp_i; trivial. erewrite sat_ext.
split; eauto. intros n. split. 2: easy. now destruct n.
Qed.
Definition P_zero := fun v => proj1_sig (@i_f_p _ _ D I Zero) (Vector.tl v) (Vector.hd v).
Definition P_succ := fun v => proj1_sig (@i_f_p _ _ D I Succ) (Vector.tl v) (Vector.hd v).
Definition P_plus := fun v => proj1_sig (@i_f_p _ _ D I Plus) (Vector.tl v) (Vector.hd v).
Definition P_mult := fun v => proj1_sig (@i_f_p _ _ D I Mult) (Vector.tl v) (Vector.hd v).
Definition P_eq := fun v => @i_P_p _ _ D I Eq v.
Lemma embed_term_funcfree_correct rho rho_f rho_p t :
first_order_term t -> forall d, @eval_p Σf Σp D I rho t d <-> sat Σf' Σp' D I' ⟨d .: get_indi_p rho, rho_f, P_zero .: P_succ .: P_plus .: P_mult .: P_eq .: rho_p⟩ (embed_term_funcfree t).
Proof.
intros F. induction t; intros d; cbn.
- split. now intros ->. intros H. now apply (H (fun v => Vector.hd v = d)).
- now exfalso.
- destruct f; repeat depelim v; cbn in *.
+ split.
* intros [v' [? ?]]. now repeat depelim v'.
* intros H. now exists ([]).
+ split.
* intros [v' [[? ?] ?]]. repeat depelim v'; cbn in *. exists h0. split.
apply sat_sshift1. apply embed_term_funcfree_funcfree. now apply IH. easy.
* intros [d1 H]. exists ([d1]). repeat split. apply IH; try easy.
eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply H. easy.
+ split.
* intros [v' [[? ?] ?]]. repeat depelim v'; cbn in *.
exists h1. split. apply sat_sshift1. apply embed_term_funcfree_funcfree. now apply IH.
exists h2. split. apply sat_sshift2. apply embed_term_funcfree_funcfree. now apply IH. easy.
* intros [d1 [H1 [d2 [H2 ?]]]]. exists ([d1 ; d2]). repeat split; try easy; apply IH; try easy.
eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply H1.
eapply sat_sshift2. apply embed_term_funcfree_funcfree. apply H2.
+ split.
* intros [v' [[? ?] ?]]. repeat depelim v'; cbn in *.
exists h1. split. apply sat_sshift1. apply embed_term_funcfree_funcfree. now apply IH.
exists h2. split. apply sat_sshift2. apply embed_term_funcfree_funcfree. now apply IH. easy.
* intros [d1 [H1 [d2 [H2 ?]]]]. exists ([d1 ; d2]). repeat split; try easy; apply IH; try easy.
eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply H1.
eapply sat_sshift2. apply embed_term_funcfree_funcfree. apply H2.
Qed.
Lemma embed_form_funcfree_correct rho rho_f rho_p phi :
first_order phi -> rho ⊨p phi <-> ⟨get_indi_p rho, rho_f, P_zero .: P_succ .: P_plus .: P_mult .: P_eq .: rho_p⟩ ⊨ embed_form_funcfree phi.
Proof.
induction phi in rho |-*; cbn; intros F.
- reflexivity.
- destruct p. now exfalso. destruct P. repeat depelim v; cbn in *. split.
+ intros [v' [[? [? ?]] ?]]. repeat depelim v'; cbn in *.
exists h1. split. now apply embed_term_funcfree_correct.
exists h2. split. apply sat_sshift1. apply embed_term_funcfree_funcfree.
now apply embed_term_funcfree_correct. easy.
+ intros [d1 [H1 [d2 [H2 ?]]]]. exists ([d1 ; d2]). repeat split; try easy.
all: eapply embed_term_funcfree_correct; try easy. apply H1.
eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply H2.
- destruct F as [F1 F2]. specialize (IHphi1 rho F1); specialize (IHphi2 rho F2).
destruct b; tauto.
- destruct q; split; cbn.
+ intros H d. specialize (H d). apply IHphi in H. apply H. easy.
+ intros H d. apply IHphi. easy. apply H.
+ intros [d H]. exists d. apply IHphi in H. apply H. easy.
+ intros [d H]. exists d. apply IHphi. easy. apply H.
- now exfalso.
- now exfalso.
Qed.
End EmbedSignatureFuncfree.
(** Now we can translate satisfiability and validity for arbitrary models
over arbitrary signatures to PA models. *)
Section PAValidSatTranslation.
Context `{Σf' : funcs_signature}.
Context `{Σp' : preds_signature}.
(* Encode axioms into formula *)
Definition PA_form :=
ax_eq_refl ∧ ax_eq_symm ∧ ax_zero_succ ∧ ax_succ_inj ∧ ax_add_zero ∧ ax_add_rec ∧ ax_mul_zero ∧ ax_mul_rec ∧ ax_ind.
Lemma PA_Model_sat_PA_form (M_PA : Model_of PA) :
M_PA ⊨ PA_form.
Proof.
repeat split; apply (M_correct M_PA); repeat (try (left; reflexivity); try right).
Qed.
Lemma PA_model_valid_iff_model_valid (phi : @form PA_funcs_signature PA_preds_signature _) :
(forall M_PA : Model_of PA, M_PA ⊨ phi) <-> (forall M' : @Model Σf' Σp', M' ⊨ (∀f(0) ∀f(1) ∀f(2) ∀f(2) ∀p(2) (embed_form 0 0 0 0 (PA_form --> phi)))).
Proof.
split.
- intros H M' rho fO fS fM fA pE.
pose (I := @B_I PA_funcs_signature PA_preds_signature _
(fun f => match f with Zero => fO | Succ => fS | Plus => fA | Mult => fM end)
(fun P => match P with Eq => pE end )).
pose (M := {| M_domain := M_domain M' ; M_interp := I |}).
eapply (embed_form_correct rho).
+ cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
+ intros H_PA. assert (forall psi, PA psi -> M ⊨ psi) as M_correct.
{ intros psi H3. repeat try destruct H3 as [<-|H3]; intros rho'; try easy; apply H_PA. }
apply (H {| M_model := M ; M_correct := M_correct |}).
- intros H M rho.
pose (I' := {| i_f _ _ := @i_f _ _ _ (M_interp M) Zero ([]) ; i_P _ _ := True |} ).
pose (M' := {| M_domain := M_domain M ; M_interp := I' |}).
pose (zero' := @i_f _ _ _ (M_interp M) Zero); pose (succ := @i_f _ _ _ (M_interp M) Succ); pose (plus := @i_f _ _ _ (M_interp M) Plus); pose (mult := @i_f _ _ _ (M_interp M) Mult); pose (equal := @i_P _ _ _ (M_interp M) Eq).
specialize (H M' rho zero' succ mult plus equal).
eapply embed_form_correct in H. apply H. apply PA_Model_sat_PA_form. clear H. cbn.
split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
Qed.
Lemma PA_model_sat_iff_model_sat (phi : @form PA_funcs_signature PA_preds_signature _) :
(exists (M_PA : Model_of PA) rho, (M_PA, rho) ⊨ phi) <-> (exists (M' : @Model Σf' Σp') rho, (M', rho) ⊨ (∃f(0) ∃f(1) ∃f(2) ∃f(2) ∃p(2) (embed_form 0 0 0 0 (PA_form ∧ phi)))).
Proof.
split.
- intros [M [rho H]].
pose (I' := @B_I Σf' Σp' _ (fun f _ => @i_f _ _ _ (M_interp M) Zero ([])) (fun P _ => True )).
pose (M' := {| M_domain := M_domain M ; M_interp := I' |}).
exists M', rho.
exists (@i_f _ _ _ (M_interp M) Zero), (@i_f _ _ _ (M_interp M) Succ), (@i_f _ _ _ (M_interp M) Mult), (@i_f _ _ _ (M_interp M) Plus), (@i_P _ _ _ (M_interp M) Eq).
eapply (embed_form_correct rho).
+ cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
+ split. repeat try split; apply (M_correct M); clear; firstorder. apply H.
- intros [M' [rho [fO [fS [fM [fA [pE H]]]]]]]; cbn -[embed_form] in H.
pose (I := @B_I PA_funcs_signature PA_preds_signature _
(fun f => match f with Zero => fO | Succ => fS | Plus => fA | Mult => fM end)
(fun P => match P with Eq => pE end )).
assert (forall psi, PA psi -> {| M_domain := M_domain M' ; M_interp := I |} ⊨ psi) as M_correct.
{ intros psi H1 rho'. repeat try destruct H1 as [<-|H1]; intros; try easy; apply H. }
pose (M := {| M_model := {| M_domain := M_domain M' ; M_interp := I |} ; M_correct := M_correct |}).
exists M, rho. eapply (embed_form_correct rho) in H. apply H.
split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
Qed.
Definition embed_PA phi := ∀f(0) ∀f(1) ∀f(2) ∀f(2) ∀p(2) (@embed_form Σf' Σp' 0 0 0 0 (PA_form --> phi)).
Lemma PA_sat_iff_empty_theory_sat (phi : @form PA_funcs_signature PA_preds_signature _) :
PA ⊨ phi <-> (fun _ => False) ⊨ embed_PA phi.
Proof.
split.
- intros H M. now apply PA_model_valid_iff_model_valid.
- intros H M. apply PA_model_valid_iff_model_valid. intros M'.
apply (H {| M_model := M' ; M_correct := (fun _ (f : False) => match f with end) |}).
Qed.
End PAValidSatTranslation.
Section PAValidSatTranslation_Funcfree.
Context `{Σf' : funcs_signature}.
Context `{Σp' : preds_signature}.
(* Encode axioms into formula *)
Definition PA_form_embedded :=
@embed_form_funcfree Σf' Σp' (ax_eq_refl ∧ ax_eq_symm ∧ ax_zero_succ ∧ ax_succ_inj ∧ ax_add_zero ∧ ax_add_rec ∧ ax_mul_zero ∧ ax_mul_rec)
∧ ∀p(1) (∃i p$1 ([$0]) ∧ p$0 ([$0])) --> (∀i p$0 ([$0]) --> (∃i p$0 ([$0 ; $1]) ∧ p$0 ([$0]))) --> ∀i p$0 ([$0]).
Definition total_functional0 x := (∃i p$x ([$0])) ∧ (∀i ∀i p$x ([$1]) --> p$x ([$0]) --> ∀p(1) p$0 ([$1]) --> p$0 ([$0])).
Definition total_functional1 x := (∀i ∃i p$x ([$0 ; $1])) ∧ (∀i ∀i ∀i p$x ([$1 ; $2]) --> p$x ([$0 ; $2]) --> ∀p(1) p$0 ([$1]) --> p$0 ([$0])).
Definition total_functional2 x := (∀i ∀i ∃i p$x ([$0 ; $1 ; $2])) ∧ (∀i ∀i ∀i ∀i p$x ([$1 ; $2 ; $3]) --> p$x ([$0 ; $2 ; $3]) --> ∀p(1) p$0 ([$1]) --> p$0 ([$0])).
Definition all_total_functional := total_functional0 0 ∧ total_functional1 0 ∧ total_functional2 0 ∧ total_functional2 1.
Lemma total_functional0_correct (M : Model) rho x :
functional (fun v d => get_pred rho x 1 (Vector.cons _ d _ v)) /\ total (fun v d => get_pred rho x 1 (Vector.cons _ d _ v)) -> (M, rho) ⊨ (total_functional0 x).
Proof.
intros [HF HT]. cbn. split.
- intros. apply HT.
- intros d1 d2 ? ?. now rewrite (HF ([]) d1 d2).
Qed.
Lemma total_functional1_correct (M : Model) rho x :
functional (fun v d => get_pred rho x 2 (Vector.cons _ d _ v)) /\ total (fun v d => get_pred rho x 2 (Vector.cons _ d _ v)) -> (M, rho) ⊨ (total_functional1 x).
Proof.
intros [HF HT]. cbn. split.
- intros. apply HT.
- intros a d1 d2 ? ?. now rewrite (HF ([a]) d1 d2).
Qed.
Lemma total_functional2_correct (M : Model) rho x :
functional (fun v d => get_pred rho x 3 (Vector.cons _ d _ v)) /\ total (fun v d => get_pred rho x 3 (Vector.cons _ d _ v)) -> (M, rho) ⊨ (total_functional2 x).
Proof.
intros [HF HT]. cbn. split.
- intros. apply HT.
- intros a1 a2 d1 d2 ? ?. now rewrite (HF ([a2 ; a1]) d1 d2).
Qed.
Lemma PA_model_valid_iff_model_valid_funcfree (phi : @form PA_funcs_signature PA_preds_signature _) :
first_order phi -> (forall M_PA : Model_p_of PA, M_PA ⊨p phi) <-> (forall M' : Model, M' ⊨ (∀p(2) ∀p(3) ∀p(3) ∀p(2) ∀p(1) all_total_functional --> PA_form_embedded --> (embed_form_funcfree phi))).
Proof.
intros FO. split.
- intros H M' rho PE PM P_A PS PO H1 H_PA. cbn [get_indi get_func get_pred] in *.
assert (functional (fun v d => PO (Vector.cons d v)) /\ total (fun v d => PO (Vector.cons d v))) as HPO.
{ destruct H1 as [[[[HF HT] _] _] _]. split. intros v y y' H2 H3. depelim v. now apply (HT y y' H2 H3 (fun v => y = Vector.hd v)). intros v. depelim v. apply HF. }
assert (functional (fun v d => PS (Vector.cons d v)) /\ total (fun v d => PS (Vector.cons d v))) as HPS.
{ destruct H1 as [[[_ [HF HT]] _] _]. split. intros v y y' H2 H3. repeat depelim v. now apply (HT h y y' H2 H3 (fun v => y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
assert (functional (fun v d => P_A (Vector.cons d v)) /\ total (fun v d => P_A (Vector.cons d v))) as HPA.
{ destruct H1 as [[[_ _] [HF HT]] _]. split. intros v y y' H2 H3. repeat depelim v. now apply (HT h0 h y y' H2 H3 (fun v => y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
assert (functional (fun v d => PM (Vector.cons d v)) /\ total (fun v d => PM (Vector.cons d v))) as HPM.
{ destruct H1 as [[[_ _] _] [HF HT]]. split. intros v y y' H2 H3. repeat depelim v. now apply (HT h0 h y y' H2 H3 (fun v => y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
Existing Instance PA_funcs_signature.
Existing Instance PA_preds_signature.
pose (I := {| i_f_p f := match f with Zero => exist _ (fun v d => PO (Vector.cons d v)) HPO | Succ => exist _ (fun v d => PS (Vector.cons d v)) HPS | Plus => exist _ (fun v d => P_A (Vector.cons d v)) HPA | Mult => exist _ (fun v d => PM (Vector.cons d v)) HPM end ;
i_P_p P := match P with Eq => PE end |}).
pose (M := {| M_p_domain := M_domain M' ; M_p_interp := I |}).
destruct rho as [rho_i rho_f rho_p]. cbn [get_indi get_func get_pred] in *.
eapply sat_ext.
2: apply (embed_form_funcfree_correct ⟨⟨rho_i, fun _ _ => default_func_p _ (rho_i 0), rho_p⟩⟩); trivial.
+ intros n. split. reflexivity. intros ar. split. reflexivity.
destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
all: now repeat depelim v.
+ assert (forall psi, PA psi -> M ⊨p psi) as M_correct.
{ destruct H_PA as [H_PA1 H_PA2]. eapply sat_ext in H_PA1. eapply (embed_form_funcfree_correct ⟨⟨rho_i, fun _ _ => default_func_p _ (rho_i 0), rho_p⟩⟩) in H_PA1.
* intros psi H2 rho. repeat destruct H2 as [<-|H2]; try easy; try apply H_PA1.
cbn. cbn in H_PA2. intros P [v1 [[[v2 [? ?]] ?] ?]] H_IH d.
repeat depelim v1. repeat depelim v2. exists ([d]). repeat split.
apply H_PA2. now exists h. intros d' ?. destruct (H_IH d') as [v3 [[[v4 [[-> ?] ?]] ?] ?]].
now exists ([d']). repeat depelim v3. repeat depelim v4. now exists h1.
* easy.
* intros n. split. reflexivity. intros ar. split. reflexivity.
destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
all: now repeat depelim v. }
apply (H {| M_p_model := M ; M_p_correct := M_correct |}).
- intros H M rho.
Existing Instance Σf'. Existing Instance Σp'.
pose (I' := {| i_f _ _ := get_indi_p rho 0 ; i_P _ _ := True |} ).
pose (M' := {| M_domain := M_p_domain M ; M_interp := I' |}).
pose (zero' := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Zero) (tl v) (hd v)); pose (succ := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Succ) (tl v) (hd v)); pose (plus := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Plus) (tl v) (hd v)); pose (mult := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Mult) (tl v) (hd v)); pose (equal := @i_P_p _ _ _ (M_p_interp M) Eq).
pose (rho' := ⟨get_indi_p rho, fun _ _ _ => get_indi_p rho 0, fun _ _ _ => True⟩).
specialize (H M' rho' equal mult plus succ zero'); change ((M', ⟨get_indi rho', get_func rho', zero' .: succ .: plus .: mult .: equal .: get_pred rho'⟩) ⊨ (all_total_functional --> PA_form_embedded --> embed_form_funcfree phi)) in H.
eapply embed_form_funcfree_correct in H. apply H. easy.
+ change ((M', ⟨get_indi rho', get_func rho', zero' .: succ .: plus .: mult .: equal .: get_pred rho'⟩) ⊨ (all_total_functional)).
split. split. split.
* apply total_functional0_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Zero).
* apply total_functional1_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Succ).
* apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Plus).
* apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Mult).
+ split.
* eapply embed_form_funcfree_correct. easy. repeat split; apply (M_p_correct M); clear; firstorder.
* cbn. intros P [d0 [? ?]] IH d. edestruct (M_p_correct M ax_ind ltac:(clear;firstorder) rho P) as [v H3].
-- exists [d0]. cbn. repeat split; trivial. now exists [].
-- cbn. intros d1 [v' [[-> ?] ?]]. repeat depelim v'. destruct (IH h) as [dS [? ?]]; trivial.
exists [dS]. repeat split; trivial. now exists [h].
-- cbn in H3. instantiate (1 := hd ([d])) in H3. repeat depelim v. cbn in H3.
now destruct H3 as [[-> ?] ?].
Qed.
Lemma PA_model_sat_iff_model_sat_funcfree (phi : @form PA_funcs_signature PA_preds_signature _) :
first_order phi -> (exists (M_PA : Model_p_of PA) rho, (M_PA, rho) ⊨p phi) <-> (exists (M' : Model) rho, (M', rho) ⊨ (∃p(2) ∃p(3) ∃p(3) ∃p(2) ∃p(1) all_total_functional ∧ PA_form_embedded ∧ (embed_form_funcfree phi))).
Proof.
intros FO. split.
- intros [M [rho H]].
pose (I' := {| i_f _ _ := get_indi_p rho 0 ; i_P _ _ := True |} ).
pose (M' := {| M_domain := M_p_domain M ; M_interp := I' |}).
pose (rho' := ⟨get_indi_p rho, fun _ _ _ => get_indi_p rho 0, fun _ _ _ => True⟩).
exists M', rho'.
pose (zero' := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Zero) (tl v) (hd v)); pose (succ := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Succ) (tl v) (hd v)); pose (plus := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Plus) (tl v) (hd v)); pose (mult := fun v => proj1_sig (@i_f_p _ _ _ (M_p_interp M) Mult) (tl v) (hd v)); pose (equal := @i_P_p _ _ _ (M_p_interp M) Eq).
exists equal, mult, plus, succ, zero'; change ((M', ⟨get_indi rho', get_func rho', zero' .: succ .: plus .: mult .: equal .: get_pred rho'⟩) ⊨ ((all_total_functional ∧ PA_form_embedded) ∧ embed_form_funcfree phi)).
split. split.
+ split. split. split.
* apply total_functional0_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Zero).
* apply total_functional1_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Succ).
* apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Plus).
* apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Mult).
+ split.
* eapply embed_form_funcfree_correct. easy. repeat split; apply (M_p_correct M); clear; firstorder.
* cbn. intros P [d0 [? ?]] IH d. edestruct (M_p_correct M ax_ind ltac:(clear;firstorder) rho P) as [v H3].
-- exists [d0]. cbn. repeat split; trivial. now exists [].
-- cbn. intros d1 [v' [[-> ?] ?]]. repeat depelim v'. destruct (IH h) as [dS [? ?]]; trivial.
exists [dS]. repeat split; trivial. now exists [h].
-- cbn in H3. instantiate (1 := hd ([d])) in H3. repeat depelim v. cbn in H3.
now destruct H3 as [[-> ?] ?].
+ now eapply embed_form_funcfree_correct.
- intros [M' [rho [PE [PM [P_A [PS [PO H]]]]]]]. cbn [get_indi get_func get_pred] in *.
destruct H as [[HTF H_PA] H].
assert (functional (fun v d => PO (Vector.cons d v)) /\ total (fun v d => PO (Vector.cons d v))) as HPO.
{ destruct HTF as [[[[HF HT] _] _] _]. split. intros v y y' H2 H3. depelim v. now apply (HT y y' H2 H3 (fun v => y = Vector.hd v)). intros v. depelim v. apply HF. }
assert (functional (fun v d => PS (Vector.cons d v)) /\ total (fun v d => PS (Vector.cons d v))) as HPS.
{ destruct HTF as [[[_ [HF HT]] _] _]. split. intros v y y' H2 H3. repeat depelim v. now apply (HT h y y' H2 H3 (fun v => y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
assert (functional (fun v d => P_A (Vector.cons d v)) /\ total (fun v d => P_A (Vector.cons d v))) as HPA.
{ destruct HTF as [[[_ _] [HF HT]] _]. split. intros v y y' H2 H3. repeat depelim v. now apply (HT h0 h y y' H2 H3 (fun v => y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
assert (functional (fun v d => PM (Vector.cons d v)) /\ total (fun v d => PM (Vector.cons d v))) as HPM.
{ destruct HTF as [[[_ _] _] [HF HT]]. split. intros v y y' H2 H3. repeat depelim v. now apply (HT h0 h y y' H2 H3 (fun v => y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
Existing Instance PA_funcs_signature.
Existing Instance PA_preds_signature.
pose (I := {| i_f_p f := match f with Zero => exist _ (fun v d => PO (Vector.cons d v)) HPO | Succ => exist _ (fun v d => PS (Vector.cons d v)) HPS | Plus => exist _ (fun v d => P_A (Vector.cons d v)) HPA | Mult => exist _ (fun v d => PM (Vector.cons d v)) HPM end ;
i_P_p P := match P with Eq => PE end |}).
pose (M := {| M_p_domain := M_domain M' ; M_p_interp := I |}).
destruct rho as [rho_i rho_f rho_p]. cbn [get_indi get_func get_pred] in *.
assert (forall psi, PA psi -> M ⊨p psi) as M_correct.
{ destruct H_PA as [H_PA1 H_PA2]. eapply sat_ext in H_PA1. eapply (embed_form_funcfree_correct ⟨⟨rho_i, fun _ _ => default_func_p _ (rho_i 0), rho_p⟩⟩) in H_PA1.
* intros psi H2 rho. repeat destruct H2 as [<-|H2]; try easy; try apply H_PA1.
cbn. cbn in H_PA2. intros P [v1 [[[v2 [? ?]] ?] ?]] H_IH d.
repeat depelim v1. repeat depelim v2. exists ([d]). repeat split.
apply H_PA2. now exists h. intros d' ?. destruct (H_IH d') as [v3 [[[v4 [[-> ?] ?]] ?] ?]].
now exists ([d']). repeat depelim v3. repeat depelim v4. now exists h1.
* easy.
* intros n. split. reflexivity. intros ar. split. reflexivity.
destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
all: now repeat depelim v. }
exists {| M_p_model := M ; M_p_correct := M_correct |}.
eapply sat_ext in H.
eapply (embed_form_funcfree_correct ⟨⟨rho_i, fun _ _ => default_func_p _ (rho_i 0), rho_p⟩⟩) in H; trivial.
+ eexists. apply H.
+ intros n. split. reflexivity. intros ar. split. reflexivity.
destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
all: now repeat depelim v.
Qed.
Definition embed_PA_funcfree phi := (∀p(2) ∀p(3) ∀p(3) ∀p(2) ∀p(1) all_total_functional --> PA_form_embedded --> (embed_form_funcfree phi)).
Lemma PA_sat_iff_empty_theory_sat_funcfree (phi : @form PA_funcs_signature PA_preds_signature _) :
first_order phi -> PA ⊨p phi <-> (fun _ => False) ⊨ embed_PA_funcfree phi.
Proof.
intros FO. split.
- intros H M. now apply PA_model_valid_iff_model_valid_funcfree.
- intros H M. apply PA_model_valid_iff_model_valid_funcfree. easy. intros M'.
apply (H {| M_model := M' ; M_correct := (fun _ (f : False) => match f with end) |}).
Qed.
End PAValidSatTranslation_Funcfree.
(** ** Categoricity *)
Section Categoricity.
Variable M1 : Model_of PA.
Variable M2 : Model_of PA.
(** Abbreviations *)
Notation D1 := (M_domain (M_model M1)).
Notation D2 := (M_domain (M_model M2)).
Notation I1 := (M_interp (M_model M1)).
Notation I2 := (M_interp (M_model M2)).
Notation eq1_sem := (eq_sem M1).
Notation eq2_sem := (eq_sem M2).
Notation "'O1'" := (@i_f _ _ D1 I1 Zero ([])).
Notation "'O2'" := (@i_f _ _ D2 I2 Zero ([])).
Notation "'S1' x" := (@i_f _ _ D1 I1 Succ ([x])) (at level 37).
Notation "'S2' x" := (@i_f _ _ D2 I2 Succ ([x])) (at level 37).
Notation "x 'i⊕1' y" := (@i_f _ _ D1 I1 Plus ([x ; y])) (at level 39).
Notation "x 'i⊕2' y" := (@i_f _ _ D2 I2 Plus ([x ; y])) (at level 39).
Notation "x 'i⊗1' y" := (@i_f _ _ D1 I1 Mult ([x ; y])) (at level 38).
Notation "x 'i⊗2' y" := (@i_f _ _ D2 I2 Mult ([x ; y])) (at level 38).
Notation "x '=1=' y" := (@i_P _ _ D1 I1 Eq ([x ; y])) (at level 40).
Notation "x '=2=' y" := (@i_P _ _ D2 I2 Eq ([x ; y])) (at level 40).
(** Definition of isomorphism *)
Inductive F : D1 -> D2 -> Prop :=
| F_O : F O1 O2
| F_S : forall x y, F x y -> F (S1 x) (S2 y).
Lemma F_inv1 x :
F (S1 x) O2 -> False.
Proof.
intros H. inversion H.
+ now apply (zero_succ M1 x).
+ now apply (zero_succ M2 y).
Qed.
Lemma F_inv2 y :
F O1 (S2 y) -> False.
Proof.
intros H. inversion H.
+ now apply (zero_succ M2 y).
+ now apply (zero_succ M1 x).
Qed.
Lemma F_inv3 y :
F O1 y -> y = O2.
Proof.
destruct (case_analysis M2 y) as [->|[y' ->]].
- easy.
- now intros H%F_inv2.
Qed.
Lemma F_inv4 x :
F x O2 -> x = O1.
Proof.
destruct (case_analysis M1 x) as [->|[x' ->]].
- easy.
- now intros H%F_inv1.
Qed.
Lemma F_inv5 :
forall x y, F (S1 x) y -> exists y', y = S2 y'.
Proof.
intros x y. destruct (case_analysis M2 y) as [->|[y' ->]].
- now intros H%F_inv1.
- intros _. now exists y'.
Qed.
Lemma F_inv6 :
forall x y, F x (S2 y) -> exists x', x = S1 x'.
Proof.
intros x y. destruct (case_analysis M1 x) as [->|[x' ->]].
- now intros H%F_inv2.
- intros _. now exists x'.
Qed.
Lemma F_inv7 x y :
F (S1 x) (S2 y) -> F x y.
Proof.
intros H. inversion H.
+ exfalso. now apply (zero_succ M1 x).
+ apply (succ_inj M1) in H0 as ->.
apply (succ_inj M2) in H1 as ->.
exact H2.
Qed.
Lemma F_total :
forall x, exists y, F x y.
Proof.
apply (induction M1).
- exists O2. exact F_O.
- intros x [y IH]. exists (S2 y). now apply F_S.
Qed.
Lemma F_surjective :
forall y, exists x, F x y.
Proof.
apply (induction M2).
- exists O1. exact F_O.
- intros y [x IH]. exists (S1 x). now apply F_S.
Qed.
Lemma F_functional :
forall x y y', F x y -> F x y' -> y = y'.
Proof.
apply (induction M1 (fun x => forall y y', F x y -> F x y' -> y = y')).
- intros y y' H1 H2. now rewrite (F_inv3 y), (F_inv3 y').
- intros x IH y y' H1 H2.