-
Notifications
You must be signed in to change notification settings - Fork 0
/
PeanoAxioms.v
1670 lines (1607 loc) · 67.7 KB
/
PeanoAxioms.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
(** The Peano axioms as a computable characteristic function nat -> bool,
which tells whether a natural number represents such an axiom. *)
Require Import PeanoNat.
Require Import Arith.Wf_nat.
Require Import Arith.Compare_dec.
Require Import EnumSeqNat.
Require Import Formulas.
Require Import Substitutions.
Require Import IsFreeForSubst.
Require Import Proofs.
Require Import ProofTactics.
(* We give more readable names to the symbols used by the Peano axioms. *)
Definition PAzero : nat := Lconst 0.
Definition PAsucc : nat -> nat := Lop1 0.
Definition PAplus : nat -> nat -> nat := Lop2 0.
Definition PAmult : nat -> nat -> nat := Lop2 1.
Definition PAle : nat -> nat -> nat := Lrel2 1. (* Lrel2 0 is Leq by convention *)
Definition PAax1 : nat := Lforall 0 (Lnot (Leq (PAsucc (Lvar 0)) PAzero)).
Definition PAax2 : nat := Lforall 0 (Lor (Leq (Lvar 0) PAzero)
(Lexists 1 (Leq (Lvar 0) (PAsucc (Lvar 1))))).
Definition PAax3 : nat :=
Lforall 0 (Lforall 1 (Limplies (Leq (PAsucc (Lvar 0)) (PAsucc (Lvar 1)))
(Leq (Lvar 0) (Lvar 1)))).
Definition PAax4 : nat := Lforall 0 (Leq (PAplus (Lvar 0) PAzero) (Lvar 0)).
Definition PAax5 : nat :=
Lforall 0 (Lforall 1 (Leq (PAplus (Lvar 0) (PAsucc (Lvar 1)))
(PAsucc (PAplus (Lvar 0) (Lvar 1))))).
Definition PAax6 : nat := Lforall 0 (Leq (PAmult (Lvar 0) PAzero) PAzero).
Definition PAax7 : nat :=
Lforall 0 (Lforall 1 (Leq (PAmult (Lvar 0) (PAsucc (Lvar 1)))
(PAplus (PAmult (Lvar 0) (Lvar 1)) (Lvar 0)))).
Definition PAorder : nat :=
Lforall 0 (Lforall 1 (Lequiv (PAle (Lvar 0) (Lvar 1))
(Lexists 2 (Leq (PAplus (Lvar 2) (Lvar 0)) (Lvar 1))))).
(* We add the Peano induction schema for the sake of completeness,
but won't use it in the rest of this repository. *)
Definition PAinduction (f : nat) : bool :=
IsLproposition f
&& IsLimplies f
&& IsLand (CoordNat f 1)
&& IsLforall (CoordNat (CoordNat f 1) 2)
&& IsLimplies (CoordNat (CoordNat (CoordNat f 1) 2) 2)
&& IsLforall (CoordNat f 2)
&& Nat.eqb (CoordNat (CoordNat (CoordNat f 1) 2) 1)
(CoordNat (CoordNat f 2) 1) (* same variable quantified *)
&& Nat.eqb (CoordNat (CoordNat (CoordNat (CoordNat f 1) 2) 2) 1)
(CoordNat (CoordNat f 2) 2)
&& Nat.eqb (CoordNat (CoordNat f 1) 1)
(Subst PAzero (CoordNat (CoordNat f 2) 1) (CoordNat (CoordNat f 2) 2))
&& Nat.eqb (CoordNat (CoordNat (CoordNat (CoordNat f 1) 2) 2) 2)
(Subst (PAsucc (Lvar (CoordNat (CoordNat f 2) 1)))
(CoordNat (CoordNat f 2) 1)
(CoordNat (CoordNat f 2) 2)).
Definition IsWeakHeytingAxiom (prop : nat) : bool :=
Nat.eqb prop PAax1
|| Nat.eqb prop PAax2
|| Nat.eqb prop PAax3
|| Nat.eqb prop PAax4
|| Nat.eqb prop PAax5
|| Nat.eqb prop PAax6
|| Nat.eqb prop PAax7
|| Nat.eqb prop PAorder.
(* Propositional axiom schema ~~X1 -> X1 *)
Definition IsPropAx4 (f : nat) : bool :=
IsLproposition f
&& IsLimplies f
&& IsLnot (CoordNat f 1)
&& IsLnot (CoordNat (CoordNat f 1) 1)
&& Nat.eqb (CoordNat (CoordNat (CoordNat f 1) 1) 1) (CoordNat f 2).
(* Peano arithmetic extends Heyting arithmetic by adding the excluded middle
axiom schema. PA is therefore one of the applications of the incompleteness
theorem. *)
Definition IsWeakPeanoAxiom (prop : nat) : bool :=
IsWeakHeytingAxiom prop || IsPropAx4 prop.
Lemma PAaxiomIsLproposition :
forall k : nat, IsWeakPeanoAxiom k = true -> IsLproposition k = true.
Proof.
intros.
apply Bool.orb_prop in H; destruct H.
apply Bool.orb_prop in H; destruct H.
apply Bool.orb_prop in H; destruct H.
apply Bool.orb_prop in H; destruct H.
apply Bool.orb_prop in H; destruct H.
apply Bool.orb_prop in H; destruct H.
apply Bool.orb_prop in H; destruct H.
apply Bool.orb_prop in H; destruct H.
- apply Nat.eqb_eq in H. subst k.
unfold PAax1. rewrite IsLproposition_forall, IsLproposition_not.
unfold Leq. rewrite IsLproposition_rel2.
unfold PAsucc, PAzero.
rewrite IsLterm_op1, IsLterm_var, IsLterm_const.
reflexivity.
- apply Nat.eqb_eq in H. subst k.
unfold PAax2. rewrite IsLproposition_forall.
unfold Leq. rewrite IsLproposition_or.
rewrite IsLproposition_rel2, IsLproposition_exists.
rewrite IsLproposition_rel2.
unfold PAsucc, PAzero.
rewrite IsLterm_op1, IsLterm_var, IsLterm_const.
rewrite IsLterm_var.
reflexivity.
- apply Nat.eqb_eq in H. subst k.
unfold PAax3. rewrite IsLproposition_forall, IsLproposition_forall.
rewrite IsLproposition_implies. apply andb_true_intro.
split. unfold Leq.
rewrite IsLproposition_rel2.
apply andb_true_intro. split.
unfold PAsucc. rewrite IsLterm_op1, IsLterm_var. reflexivity.
unfold PAsucc. rewrite IsLterm_op1, IsLterm_var. reflexivity.
unfold Leq.
rewrite IsLproposition_rel2.
apply andb_true_intro. split.
unfold PAsucc. rewrite IsLterm_var. reflexivity.
unfold PAsucc. rewrite IsLterm_var. reflexivity.
- apply Nat.eqb_eq in H. subst k.
unfold PAax4. rewrite IsLproposition_forall.
unfold Leq.
rewrite IsLproposition_rel2.
apply andb_true_intro. split.
unfold PAplus. rewrite IsLterm_op2.
apply andb_true_intro. split.
rewrite IsLterm_var. reflexivity.
unfold PAzero.
rewrite IsLterm_const. reflexivity.
rewrite IsLterm_var. reflexivity.
- apply Nat.eqb_eq in H. subst k.
unfold PAax5.
rewrite IsLproposition_forall, IsLproposition_forall.
unfold Leq. rewrite IsLproposition_rel2.
apply andb_true_intro. split.
unfold PAplus. rewrite IsLterm_op2.
apply andb_true_intro. split.
rewrite IsLterm_var. reflexivity.
unfold PAsucc. rewrite IsLterm_op1, IsLterm_var. reflexivity.
unfold PAsucc. rewrite IsLterm_op1.
unfold PAplus. rewrite IsLterm_op2.
apply andb_true_intro. split.
rewrite IsLterm_var. reflexivity.
rewrite IsLterm_var. reflexivity.
- apply Nat.eqb_eq in H. subst k.
unfold PAax6, Leq.
rewrite IsLproposition_forall, IsLproposition_rel2.
apply andb_true_intro; split.
unfold PAmult. rewrite IsLterm_op2.
apply andb_true_intro; split.
apply IsLterm_var.
unfold PAzero.
rewrite IsLterm_const. reflexivity.
unfold PAzero.
rewrite IsLterm_const. reflexivity.
- apply Nat.eqb_eq in H. subst k.
unfold PAax7, Leq.
rewrite IsLproposition_forall, IsLproposition_forall.
rewrite IsLproposition_rel2.
apply andb_true_intro; split.
unfold PAmult. rewrite IsLterm_op2.
apply andb_true_intro; split.
apply IsLterm_var.
unfold PAsucc. rewrite IsLterm_op1. apply IsLterm_var.
unfold PAplus. rewrite IsLterm_op2.
apply andb_true_intro; split.
2: apply IsLterm_var.
unfold PAmult. rewrite IsLterm_op2.
apply andb_true_intro; split; apply IsLterm_var.
- apply Nat.eqb_eq in H. subst k.
unfold PAorder, PAle.
rewrite IsLproposition_forall, IsLproposition_forall.
rewrite IsLproposition_equiv.
apply andb_true_intro; split.
rewrite IsLproposition_rel2.
apply andb_true_intro; split.
apply IsLterm_var.
apply IsLterm_var.
rewrite IsLproposition_exists.
unfold Leq. rewrite IsLproposition_rel2.
apply andb_true_intro; split.
2: apply IsLterm_var.
unfold PAplus. rewrite IsLterm_op2.
apply andb_true_intro; split; apply IsLterm_var.
- do 4 (apply andb_prop in H; destruct H).
exact H.
Qed.
(** Test functions that formulas only use the Peano symbols. *)
Definition IsPeanoTermRec (t : nat) (rec : nat -> bool) : bool :=
match CoordNat t 0 with
| LvarHead => IsLvar t
| LopHead => match CoordNat t 1 with
| 0 => (* PAzero or PAsucc or PAplus *)
Nat.eqb (LengthNat t) 2
|| Nat.eqb (LengthNat t) 3 && rec 2
|| Nat.eqb (LengthNat t) 4 && rec 2 && rec 3
| 1 => (* PAmult *)
Nat.eqb (LengthNat t) 4 && rec 2 && rec 3
| _ => false
end
&& Nat.leb 2 (LengthNat t)
&& Nat.eqb (NthTailNat t (LengthNat t)) 0
| _ => false
end.
Definition IsPeanoTerm : nat -> bool := TreeFoldNat IsPeanoTermRec false.
Lemma IsPeanoTerm_step : forall t,
IsPeanoTerm t = TreeFoldNatRec IsPeanoTermRec false t (fun k _ => IsPeanoTerm k).
Proof.
intros.
unfold IsPeanoTerm, TreeFoldNat. rewrite Fix_eq.
reflexivity.
intros. unfold TreeFoldNatRec, IsPeanoTermRec.
destruct (le_lt_dec (LengthNat x) 0). reflexivity.
destruct (CoordNat x 0). reflexivity.
repeat (destruct n; [reflexivity|]).
destruct n. rewrite H, H. reflexivity.
destruct n; reflexivity.
Qed.
Lemma IsPeanoTerm_PAzero : IsPeanoTerm PAzero = true.
Proof.
intros. rewrite IsPeanoTerm_step.
unfold TreeFoldNatRec.
destruct (le_lt_dec (LengthNat PAzero) 0).
unfold PAzero in l. rewrite LengthLconst in l. inversion l.
unfold IsPeanoTermRec.
unfold PAzero, Lconst, Lop.
rewrite CoordConsHeadNat.
rewrite CoordConsTailNat, CoordConsHeadNat.
rewrite LengthConsNat, LengthConsNat. simpl.
do 2 rewrite TailConsNat. reflexivity.
Qed.
Lemma IsPeanoTerm_PAsucc : forall n,
IsPeanoTerm (PAsucc n) = IsPeanoTerm n.
Proof.
intros. rewrite IsPeanoTerm_step.
unfold TreeFoldNatRec.
destruct (le_lt_dec (LengthNat (PAsucc n)) 0).
unfold PAsucc,Lop1 in l. rewrite LengthLop in l. inversion l.
unfold IsPeanoTermRec.
unfold PAsucc, Lop1, Lop.
rewrite CoordConsHeadNat.
rewrite CoordConsTailNat, CoordConsHeadNat.
rewrite LengthConsNat, LengthConsNat, LengthConsNat. simpl.
do 2 rewrite CoordConsTailNat.
rewrite CoordConsHeadNat.
do 3 rewrite TailConsNat. simpl.
destruct (IsPeanoTerm n); reflexivity.
Qed.
Lemma IsPeanoTerm_PAmult : forall n m,
IsPeanoTerm (PAmult n m) = (IsPeanoTerm n && IsPeanoTerm m)%bool.
Proof.
intros. rewrite IsPeanoTerm_step.
unfold TreeFoldNatRec.
destruct (le_lt_dec (LengthNat (PAmult n m)) 0).
unfold PAmult, Lop2 in l. rewrite LengthLop in l. inversion l.
unfold IsPeanoTermRec.
unfold PAmult, Lop2, Lop.
rewrite CoordConsHeadNat.
rewrite CoordConsTailNat, CoordConsHeadNat.
do 4 rewrite LengthConsNat. simpl.
do 5 rewrite CoordConsTailNat.
rewrite CoordConsHeadNat.
rewrite CoordConsHeadNat.
do 4 rewrite TailConsNat. simpl.
destruct (IsPeanoTerm n), (IsPeanoTerm m); reflexivity.
Qed.
Lemma PeanoTermIsLterm : forall t,
IsPeanoTerm t = true -> IsLterm t = true.
Proof.
apply (Fix lt_wf (fun t => IsPeanoTerm t = true -> IsLterm t = true)).
intros t IHt tpeano.
rewrite IsPeanoTerm_step in tpeano.
unfold TreeFoldNatRec in tpeano.
rewrite IsLterm_step. unfold TreeFoldNatRec.
destruct (le_lt_dec (LengthNat t) 0). discriminate tpeano.
unfold IsLtermRec.
unfold IsPeanoTermRec in tpeano.
destruct (CoordNat t 0) eqn:headT. discriminate tpeano.
repeat (destruct n; [discriminate tpeano|]).
destruct n.
- (* Lop *)
apply andb_prop in tpeano. destruct tpeano.
apply andb_prop in H. destruct H.
apply andb_true_intro. split. 2: exact H0.
apply IsLopTerm_spec. apply Nat.leb_le in H1.
split. exact H1. split. exact H1.
intros j H2. apply IHt.
exact (CoordLower _ _ (LengthPositive _ l)).
destruct H2. destruct j. inversion H2.
destruct j. apply le_S_n in H2. inversion H2. clear H2.
destruct (CoordNat t 1) eqn:op.
+ apply Bool.orb_prop in H. destruct H.
apply Bool.orb_prop in H. destruct H.
apply Nat.eqb_eq in H. rewrite H in H3.
exfalso. apply le_S_n, le_S_n in H3. inversion H3.
apply andb_prop in H. destruct H.
apply Nat.eqb_eq in H. rewrite H in H3.
destruct j. exact H2.
apply le_S_n, le_S_n, le_S_n in H3. inversion H3.
apply andb_prop in H. destruct H.
apply andb_prop in H. destruct H.
apply Nat.eqb_eq in H. rewrite H in H3.
destruct j. exact H4.
destruct j. exact H2. do 4 apply le_S_n in H3. inversion H3.
+ destruct n. 2: discriminate H.
apply andb_prop in H. destruct H.
apply andb_prop in H. destruct H.
apply Nat.eqb_eq in H. rewrite H in H3.
destruct j. exact H4.
destruct j. exact H2. do 4 apply le_S_n in H3. inversion H3.
- (* Lvar *) exact tpeano.
Qed.
Definition IsPeanoPropositionRec (f : nat) (rec : nat -> bool) : bool :=
match CoordNat f 0 with
| LnotHead => IsLnot f && rec 1
| LimpliesHead => IsLimplies f && rec 1 && rec 2
| LorHead => IsLor f && rec 1 && rec 2
| LandHead => IsLand f && rec 1 && rec 2
| LforallHead => IsLforall f && rec 2
| LexistsHead => IsLexists f && rec 2
| LrelHead => Nat.eqb (LengthNat f) 4
&& (Nat.eqb (CoordNat f 1) 0 || Nat.eqb (CoordNat f 1) 1)
&& IsPeanoTerm (CoordNat f 2)
&& IsPeanoTerm (CoordNat f 3)
&& Nat.eqb (NthTailNat f (LengthNat f)) 0
| _ => false
end.
Definition IsPeanoProposition : nat -> bool := TreeFoldNat IsPeanoPropositionRec false.
Lemma IsPeanoProposition_step : forall p,
IsPeanoProposition p = TreeFoldNatRec IsPeanoPropositionRec false p
(fun k _ => IsPeanoProposition k).
Proof.
intros.
unfold IsPeanoProposition, TreeFoldNat. rewrite Fix_eq.
reflexivity.
intros. unfold IsPeanoPropositionRec, TreeFoldNatRec.
destruct (le_lt_dec (LengthNat x) 0). reflexivity.
destruct (CoordNat x 0). reflexivity.
destruct n. rewrite H. reflexivity.
destruct n. rewrite H, H. reflexivity.
destruct n. rewrite H, H. reflexivity.
destruct n. rewrite H, H. reflexivity.
destruct n. rewrite H. reflexivity.
destruct n. rewrite H. reflexivity.
destruct n. reflexivity. reflexivity.
Qed.
Lemma PeanoProposition_rect : forall (A : nat -> Type),
(forall (t u:nat)
(tterm : IsPeanoTerm t = true)
(uterm : IsPeanoTerm u = true),
A (Leq t u))
-> (forall (t u:nat)
(tterm : IsPeanoTerm t = true)
(uterm : IsPeanoTerm u = true),
A (PAle t u))
-> (forall (prop:nat) (propprop : IsPeanoProposition prop = true)
(IHprop : A prop), A (Lnot prop))
-> (forall (g h:nat)
(gprop : IsPeanoProposition g = true)
(hprop : IsPeanoProposition h = true)
(IHg : A g) (IHh : A h), A (Limplies g h))
-> (forall (g h:nat)
(gprop : IsPeanoProposition g = true)
(hprop : IsPeanoProposition h = true)
(IHg : A g) (IHh : A h), A (Lor g h))
-> (forall (g h:nat)
(gprop : IsPeanoProposition g = true)
(hprop : IsPeanoProposition h = true)
(IHg : A g) (IHh : A h), A (Land g h))
-> (forall (v prop:nat) (propprop : IsPeanoProposition prop = true)
(IHprop : A prop), A (Lforall v prop))
-> (forall (v prop:nat) (propprop : IsPeanoProposition prop = true)
(IHprop : A prop), A (Lexists v prop))
-> forall prop, IsPeanoProposition prop = true -> A prop.
Proof.
intros A eqcase lecase notcase impliescase orcase andcase forallcase existscase.
apply (Fix lt_wf (fun prop => IsPeanoProposition prop = true -> A prop)).
intros prop IHprop propprop.
rewrite IsPeanoProposition_step in propprop.
unfold TreeFoldNatRec in propprop.
destruct (le_lt_dec (LengthNat prop) 0). discriminate propprop.
unfold IsPeanoPropositionRec in propprop.
destruct (CoordNat prop 0) eqn:headProp. discriminate propprop.
destruct n.
(* Lnot *)
apply andb_prop in propprop. destruct propprop.
apply Nat.eqb_eq in H. rewrite H. apply notcase, IHprop.
exact H0.
exact (CoordLower _ _ (LengthPositive _ l)). exact H0.
destruct n.
(* Limplies *)
apply andb_prop in propprop. destruct propprop.
apply andb_prop in H. destruct H.
apply Nat.eqb_eq in H. rewrite H. apply impliescase, IHprop.
exact H1. exact H0. apply IHprop.
exact (CoordLower _ _ (LengthPositive _ l)). exact H1.
exact (CoordLower _ _ (LengthPositive _ l)). exact H0.
destruct n.
(* Lor *)
apply andb_prop in propprop. destruct propprop.
apply andb_prop in H. destruct H.
apply Nat.eqb_eq in H. rewrite H. apply orcase, IHprop.
exact H1. exact H0. apply IHprop.
exact (CoordLower _ _ (LengthPositive _ l)). exact H1.
exact (CoordLower _ _ (LengthPositive _ l)). exact H0.
destruct n.
(* Land *)
apply andb_prop in propprop. destruct propprop.
apply andb_prop in H. destruct H.
apply Nat.eqb_eq in H. rewrite H. apply andcase, IHprop.
exact H1. exact H0. apply IHprop.
exact (CoordLower _ _ (LengthPositive _ l)). exact H1.
exact (CoordLower _ _ (LengthPositive _ l)). exact H0.
destruct n.
(* Lforall *)
apply andb_prop in propprop. destruct propprop.
apply Nat.eqb_eq in H. rewrite H.
apply forallcase, IHprop. exact H0.
exact (CoordLower _ _ (LengthPositive _ l)). exact H0.
destruct n.
(* Lexists *)
apply andb_prop in propprop. destruct propprop.
apply Nat.eqb_eq in H. rewrite H.
apply existscase, IHprop. exact H0.
exact (CoordLower _ _ (LengthPositive _ l)). exact H0.
destruct n.
(* Leq and PAle, base cases withtout IHprop *)
2: discriminate propprop. clear IHprop.
apply andb_prop in propprop. destruct propprop as [propprop proptrunc].
apply andb_prop in propprop. destruct propprop as [propprop H].
apply andb_prop in propprop. destruct propprop as [propprop H0].
apply andb_prop in propprop. destruct propprop as [lenprop eqle].
apply Nat.eqb_eq in lenprop.
rewrite HeadTailDecompNat. 2: rewrite lenprop; apply le_n_S, le_0_n.
rewrite (HeadTailDecompNat (TailNat prop)), CoordTailNat.
rewrite (HeadTailDecompNat (TailNat (TailNat prop))), CoordTailNat, CoordTailNat.
rewrite (HeadTailDecompNat (TailNat (TailNat (TailNat prop)))).
rewrite CoordTailNat, CoordTailNat, CoordTailNat.
apply Nat.eqb_eq in proptrunc. rewrite lenprop in proptrunc.
simpl in proptrunc. rewrite proptrunc. clear proptrunc.
rewrite headProp.
destruct (CoordNat prop 1 =? 0) eqn:iseq. clear eqle.
apply Nat.eqb_eq in iseq. rewrite iseq.
apply eqcase; assumption. clear iseq. simpl in eqle.
apply Nat.eqb_eq in eqle. rewrite eqle.
apply lecase; assumption.
rewrite LengthTailNat, LengthTailNat, LengthTailNat, lenprop.
apply Nat.le_refl.
rewrite LengthTailNat, LengthTailNat, lenprop.
apply le_S, Nat.le_refl.
rewrite LengthTailNat, lenprop.
apply le_S, le_S, Nat.le_refl.
Qed.
Lemma PeanoPropositionIsLproposition : forall prop,
IsPeanoProposition prop = true -> IsLproposition prop = true.
Proof.
apply PeanoProposition_rect.
- intros. rewrite IsLproposition_eq, PeanoTermIsLterm, PeanoTermIsLterm.
reflexivity. exact uterm. exact tterm.
- intros. unfold PAle.
rewrite IsLproposition_rel2, PeanoTermIsLterm, PeanoTermIsLterm.
reflexivity. exact uterm. exact tterm.
- intros. rewrite IsLproposition_not. exact IHprop.
- intros. rewrite IsLproposition_implies, IHg, IHh. reflexivity.
- intros. rewrite IsLproposition_or, IHg, IHh. reflexivity.
- intros. rewrite IsLproposition_and, IHg, IHh. reflexivity.
- intros. rewrite IsLproposition_forall. exact IHprop.
- intros. rewrite IsLproposition_exists. exact IHprop.
Qed.
(** PAnat, the injection of the meta-theoretic type nat as syntactical terms
of Peano arithmetic. *)
Fixpoint PAnat (n : nat) : nat :=
match n with
| O => PAzero
| S p => PAsucc (PAnat p)
end.
Lemma IsLterm_PAnat : forall n, IsLterm (PAnat n) = true.
Proof.
induction n.
- simpl. apply IsLterm_const.
- simpl. unfold PAsucc. rewrite IsLterm_op1. apply IHn.
Qed.
Lemma IsPeanoTerm_PAnat : forall n,
IsPeanoTerm (PAnat n) = true.
Proof.
induction n.
- simpl. apply IsPeanoTerm_PAzero.
- simpl. rewrite IsPeanoTerm_PAsucc. exact IHn.
Qed.
Lemma PAnat_closed : forall i v, VarOccursInTerm v (PAnat i) = false.
Proof.
induction i.
- intros. simpl. unfold PAzero. rewrite VarOccursInTerm_const. reflexivity.
- intros. simpl. unfold PAsucc. rewrite VarOccursInTerm_op1. apply IHi.
Qed.
Lemma IsFreeForSubst_PAnat : forall n v f,
IsLproposition f = true
-> IsFreeForSubst (PAnat n) v f = true.
Proof.
intros. apply IsFreeForSubst_closed.
exact H. intros. apply PAnat_closed.
Qed.
Lemma MaxVarTerm_PAnat : forall n, MaxVarTerm (PAnat n) = 0.
Proof.
induction n. simpl.
unfold PAzero, Lconst.
rewrite MaxVarTerm_op. simpl; rewrite LengthNilNat. reflexivity.
simpl. unfold PAsucc, Lop1.
rewrite MaxVarTerm_op. simpl.
rewrite LengthConsNat, LengthNilNat. simpl.
unfold Lop. rewrite CoordConsTailNat, CoordConsTailNat.
rewrite CoordConsHeadNat. exact IHn.
Qed.
Lemma PAinductionIsInduction : forall f : nat,
IsLproposition f = true
-> PAinduction (Limplies (Land (Subst PAzero 0 f)
(Lforall 0 (Limplies f (Subst (PAsucc (Lvar 0)) 0 f))))
(Lforall 0 f)) = true.
Proof.
intros f H.
apply andb_true_intro; split.
apply andb_true_intro; split.
apply andb_true_intro; split.
apply andb_true_intro; split.
apply andb_true_intro; split.
apply andb_true_intro; split.
apply andb_true_intro; split.
apply andb_true_intro; split.
apply andb_true_intro; split.
- rewrite IsLproposition_implies.
apply andb_true_intro; split.
rewrite IsLproposition_and.
apply andb_true_intro; split.
apply SubstIsLproposition. exact H.
unfold PAzero. apply IsLterm_const.
rewrite IsLproposition_forall.
rewrite IsLproposition_implies.
apply andb_true_intro; split. exact H.
apply SubstIsLproposition. exact H.
unfold PAsucc. rewrite IsLterm_op1. apply IsLterm_var.
rewrite IsLproposition_forall. exact H.
- apply LimpliesIsImplies.
- rewrite CoordNat_implies_1. apply LandIsAnd.
- rewrite CoordNat_implies_1, CoordNat_and_2.
apply LforallIsForall.
- rewrite CoordNat_implies_1, CoordNat_and_2.
rewrite CoordNat_forall_2. apply LimpliesIsImplies.
- rewrite CoordNat_implies_2. apply LforallIsForall.
- rewrite CoordNat_implies_2, CoordNat_implies_1.
rewrite CoordNat_and_2, CoordNat_forall_1, CoordNat_forall_1.
reflexivity.
- rewrite CoordNat_implies_2, CoordNat_implies_1.
rewrite CoordNat_and_2, CoordNat_forall_2.
rewrite CoordNat_implies_1, CoordNat_forall_2.
apply PeanoNat.Nat.eqb_refl.
- rewrite CoordNat_implies_2, CoordNat_implies_1.
rewrite CoordNat_and_1, CoordNat_forall_1, CoordNat_forall_2.
apply PeanoNat.Nat.eqb_refl.
- rewrite CoordNat_implies_2, CoordNat_implies_1.
rewrite CoordNat_and_2, CoordNat_forall_2.
rewrite CoordNat_implies_2.
rewrite CoordNat_forall_1, CoordNat_forall_2.
apply PeanoNat.Nat.eqb_refl.
Qed.
Lemma Subst_PAle : forall t v n k,
Subst t v (PAle n k) = PAle (SubstTerm t v n) (SubstTerm t v k).
Proof.
intros. unfold PAle. rewrite Subst_rel2. reflexivity.
Qed.
Lemma SubstTerm_PAzero : forall t v, SubstTerm t v PAzero = PAzero.
Proof.
intros. unfold PAzero. rewrite SubstTerm_const. reflexivity.
Qed.
Lemma SubstTerm_PAsucc : forall u v t,
SubstTerm u v (PAsucc t) = PAsucc (SubstTerm u v t).
Proof.
intros. apply SubstTerm_op1.
Qed.
Lemma SubstTerm_PAnat : forall i u v,
SubstTerm u v (PAnat i) = PAnat i.
Proof.
induction i.
- intros. simpl. unfold PAzero. apply SubstTerm_const.
- intros. simpl. rewrite SubstTerm_PAsucc, IHi. reflexivity.
Qed.
Lemma SubstTerm_PAplus : forall u v t w,
SubstTerm u v (PAplus t w) = PAplus (SubstTerm u v t) (SubstTerm u v w).
Proof.
intros. apply SubstTerm_op2.
Qed.
Lemma SubstTerm_PAmult : forall u v t w,
SubstTerm u v (PAmult t w) = PAmult (SubstTerm u v t) (SubstTerm u v w).
Proof.
intros. apply SubstTerm_op2.
Qed.
Lemma PAplus_zero : forall t,
IsLterm t = true
-> IsProved IsWeakHeytingAxiom (Leq (PAplus t PAzero) t).
Proof.
intros.
pose proof (LforallElim IsWeakHeytingAxiom
(Leq (PAplus (Lvar 0) PAzero) (Lvar 0))
0 t) as felim.
rewrite Subst_eq, SubstTerm_PAplus in felim.
rewrite SubstTerm_var in felim. simpl in felim.
unfold PAzero in felim at 3. rewrite SubstTerm_const in felim.
apply felim. 2: exact H.
apply AxiomIsProved.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; right.
unfold PAax4. apply Nat.eqb_refl.
rewrite IsLproposition_forall. unfold Leq. rewrite IsLproposition_rel2.
unfold PAplus, PAzero.
rewrite IsLterm_op2, IsLterm_var, IsLterm_const. reflexivity.
unfold Leq.
rewrite IsFreeForSubst_rel2. reflexivity.
Qed.
Lemma PAmult_zero : forall t,
IsLterm t = true
-> IsProved IsWeakHeytingAxiom (Leq (PAmult t PAzero) PAzero).
Proof.
intros.
pose proof (LforallElim IsWeakHeytingAxiom
(Leq (PAmult (Lvar 0) PAzero) PAzero)
0 t) as felim.
rewrite Subst_eq, SubstTerm_PAmult in felim.
rewrite SubstTerm_var in felim. simpl in felim.
rewrite SubstTerm_PAzero in felim.
apply felim. 2: exact H.
apply AxiomIsProved.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; right.
unfold PAax6. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_eq.
unfold PAmult, PAzero.
rewrite IsLterm_op2, IsLterm_var, IsLterm_const. reflexivity.
unfold Leq.
rewrite IsFreeForSubst_rel2. reflexivity.
Qed.
Lemma IsProvedAx1
: IsProved IsWeakHeytingAxiom
(Lforall 0 (Lnot (Leq (PAsucc (Lvar 0)) PAzero))).
Proof.
apply AxiomIsProved.
do 7 (apply Bool.orb_true_intro; left).
unfold PAax1. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_not, IsLproposition_eq.
unfold PAzero, PAsucc. rewrite IsLterm_const.
rewrite IsLterm_op1, IsLterm_var. reflexivity.
Qed.
Lemma IsProvedAx2 : forall t,
IsLterm t = true
-> VarOccursInTerm 1 t = false
-> IsProved IsWeakHeytingAxiom
(Lor (Leq t PAzero) (Lexists 1 (Leq t (PAsucc (Lvar 1))))).
Proof.
assert (IsProved IsWeakHeytingAxiom (Lforall 0 (Lor (Leq (Lvar 0) PAzero)
(Lexists 1 (Leq (Lvar 0) (PAsucc (Lvar 1))))))).
apply AxiomIsProved.
do 6 (apply Bool.orb_true_intro; left).
apply Bool.orb_true_intro; right.
unfold PAax2. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_or, IsLproposition_eq.
rewrite IsLproposition_exists, IsLproposition_eq, IsLterm_var.
unfold PAsucc. rewrite IsLterm_op1, IsLterm_var.
simpl. unfold PAzero. rewrite IsLterm_const.
reflexivity.
intros.
apply (LforallElim _ _ 0 t) in H.
rewrite Subst_or, Subst_eq, Subst_exists in H. simpl in H.
rewrite Subst_eq, SubstTerm_var in H. simpl in H.
rewrite SubstTerm_PAzero, SubstTerm_PAsucc, SubstTerm_var in H. simpl in H.
exact H. exact H0. unfold Leq.
rewrite IsFreeForSubst_or, IsFreeForSubst_rel2, IsFreeForSubst_exists.
rewrite IsFreeForSubst_rel2, H1. simpl.
rewrite Bool.orb_true_intro. reflexivity.
right. reflexivity.
Qed.
Lemma IsProvedAx3 :
IsProved IsWeakHeytingAxiom
(Lforall 0 (Lforall 1 (Limplies (Leq (PAsucc (Lvar 0)) (PAsucc (Lvar 1)))
(Leq (Lvar 0) (Lvar 1))))).
Proof.
apply AxiomIsProved.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; right.
unfold PAax3. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_forall.
rewrite IsLproposition_implies, IsLproposition_eq.
unfold PAsucc. rewrite IsLterm_op1, IsLterm_op1, IsLproposition_eq.
rewrite IsLterm_var, IsLterm_var. reflexivity.
Qed.
Lemma IsProvedAx4 :
IsProved IsWeakHeytingAxiom
(Lforall 0 (Leq (PAplus (Lvar 0) PAzero) (Lvar 0))).
Proof.
apply AxiomIsProved.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; right.
unfold PAax4. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_eq.
unfold PAplus, PAzero.
rewrite IsLterm_op2, IsLterm_var, IsLterm_const.
reflexivity.
Qed.
Lemma IsProvedAx5
: IsProved IsWeakHeytingAxiom
(Lforall 0 (Lforall 1 (Leq (PAplus (Lvar 0) (PAsucc (Lvar 1)))
(PAsucc (PAplus (Lvar 0) (Lvar 1)))))).
Proof.
apply AxiomIsProved.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; right.
unfold PAax5. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_forall.
unfold Leq.
rewrite IsLproposition_rel2.
unfold PAplus, PAsucc. rewrite IsLterm_op2, IsLterm_op1, IsLterm_op1.
rewrite IsLterm_op2, IsLterm_var, IsLterm_var. reflexivity.
Qed.
Lemma IsProvedAx7 : IsProved IsWeakHeytingAxiom
(Lforall 0 (Lforall 1 (Leq (PAmult (Lvar 0) (PAsucc (Lvar 1)))
(PAplus (PAmult (Lvar 0) (Lvar 1)) (Lvar 0))))).
Proof.
apply AxiomIsProved.
apply Bool.orb_true_intro; left.
apply Bool.orb_true_intro; right.
unfold PAax7. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_forall, IsLproposition_eq.
unfold PAplus, PAsucc, PAmult. rewrite IsLterm_op2, IsLterm_op2, IsLterm_op1.
rewrite IsLterm_op2, IsLterm_var, IsLterm_var. reflexivity.
Qed.
(* Specialization of PAle on arbitrary terms t and u. *)
Lemma IsProvedLe : forall t u,
IsLterm t = true
-> IsLterm u = true
-> VarOccursInTerm 2 t = false
-> VarOccursInTerm 2 u = false
-> IsProved IsWeakHeytingAxiom
(Lequiv (PAle t u)
(Lexists 2 (Leq (PAplus (Lvar 2) t) u))).
Proof.
assert (IsProved IsWeakHeytingAxiom
(Lforall 0 (Lforall 1 (Lequiv (PAle (Lvar 0) (Lvar 1))
(Lexists 2 (Leq (PAplus (Lvar 2) (Lvar 0)) (Lvar 1))))))).
apply AxiomIsProved.
apply Bool.orb_true_intro; right.
unfold PAorder. apply Nat.eqb_refl.
rewrite IsLproposition_forall, IsLproposition_forall.
rewrite IsLproposition_equiv, IsLproposition_exists, IsLproposition_eq.
unfold PAplus, PAsucc, PAmult, PAle.
rewrite IsLterm_op2, IsLterm_var, IsLterm_var, IsLproposition_rel2.
rewrite IsLterm_var, IsLterm_var.
reflexivity.
intros t u. intros.
pose (S (S (S (Nat.max (MaxVarTerm u) (MaxVarTerm t))))) as m.
assert (S m =? m = false).
{ apply Nat.eqb_neq. intro abs. apply (Nat.lt_irrefl m).
rewrite <- abs at 2. apply Nat.le_refl. }
apply (LforallElim _ _ 0 (Lvar m)) in H.
rewrite Subst_forall in H. simpl in H.
apply (LforallElim _ _ 1 (Lvar (S m))) in H.
rewrite Subst_equiv, Subst_equiv, Subst_PAle, Subst_PAle in H.
rewrite Subst_exists, Subst_exists in H. simpl in H.
rewrite SubstTerm_var, SubstTerm_var in H. simpl in H.
rewrite SubstTerm_var, Subst_eq, Subst_eq in H. simpl in H.
rewrite SubstTerm_PAplus, SubstTerm_var, SubstTerm_var in H. simpl in H.
rewrite SubstTerm_var, SubstTerm_var in H. simpl in H.
rewrite SubstTerm_PAplus, SubstTerm_var, SubstTerm_var in H. simpl in H.
rewrite SubstTerm_var in H. simpl in H.
apply (LforallIntro _ _ m) in H.
apply (LforallElim _ _ m t) in H.
rewrite Subst_equiv, Subst_PAle, Subst_exists in H. simpl in H.
rewrite SubstTerm_var, SubstTerm_var, Nat.eqb_refl, H4 in H.
rewrite Subst_eq, SubstTerm_var, H4 in H.
rewrite SubstTerm_PAplus, SubstTerm_var in H. simpl in H.
rewrite SubstTerm_var, Nat.eqb_refl in H. simpl in H.
apply (LforallIntro _ _ (S m)) in H.
apply (LforallElim _ _ (S m) u) in H.
rewrite Subst_equiv, Subst_PAle, Subst_exists in H. simpl in H.
rewrite SubstTerm_var, Nat.eqb_refl in H.
rewrite Subst_eq, SubstTerm_var, Nat.eqb_refl in H.
rewrite SubstTerm_PAplus, SubstTerm_var in H. simpl in H.
rewrite SubstTerm_nosubst in H. exact H.
apply MaxVarTermDoesNotOccur.
apply le_n_S, le_S, le_S, le_S, Nat.le_max_r.
exact H0. exact H1. unfold PAle, Leq.
rewrite IsFreeForSubst_equiv, IsFreeForSubst_rel2, IsFreeForSubst_exists.
rewrite IsFreeForSubst_rel2, H3.
simpl (true && negb false)%bool. rewrite Bool.orb_true_r. reflexivity.
exact H0. unfold PAle, Leq.
rewrite IsFreeForSubst_equiv, IsFreeForSubst_rel2, IsFreeForSubst_exists.
rewrite IsFreeForSubst_rel2, H2.
simpl (true && negb false)%bool. rewrite Bool.orb_true_r. reflexivity.
apply IsLterm_var.
rewrite Subst_equiv, IsFreeForSubst_equiv, Subst_PAle, Subst_exists.
simpl. unfold PAle.
rewrite IsFreeForSubst_rel2, IsFreeForSubst_exists, Subst_eq.
unfold Leq. rewrite IsFreeForSubst_rel2, VarOccursInTerm_var.
simpl. rewrite Bool.orb_true_r. reflexivity.
apply IsLterm_var.
rewrite IsFreeForSubst_forall.
apply Bool.orb_true_intro. right.
rewrite IsFreeForSubst_equiv.
unfold PAle. rewrite IsFreeForSubst_rel2, IsFreeForSubst_exists.
unfold Leq. rewrite IsFreeForSubst_rel2. simpl.
rewrite VarOccursInTerm_var, VarOccursInTerm_var.
simpl (negb (2 =? m)). rewrite Bool.orb_true_r. reflexivity.
Qed.
Lemma LeqElimSubstVarPAnat : forall IsAxiom v k prop,
IsLproposition prop = true
-> IsProved IsAxiom (Subst (PAnat k) v prop)
-> IsProved IsAxiom (Limplies (Leq (Lvar v) (PAnat k)) prop).
Proof.
intros.
apply LeqElimSubstVar. exact H.
apply IsLterm_PAnat. apply IsFreeForSubst_PAnat.
exact H. exact H0.
Qed.
(* Closed terms are proved equal to closed terms with the successor symbol only. *)
Lemma PAplus_normalize : forall i j,
IsProved IsWeakHeytingAxiom (Leq (PAplus (PAnat i) (PAnat j)) (PAnat (i + j))).
Proof.
induction j.
rewrite Nat.add_0_r. apply PAplus_zero.
apply IsLterm_PAnat.
simpl. rewrite Nat.add_succ_r. simpl.
apply (LeqTrans _ _ (PAsucc (PAplus (PAnat i) (PAnat j)))).
2: apply LeqElim_op1, IHj.
pose proof (LforallElim IsWeakHeytingAxiom
(Leq (PAplus (PAnat i) (PAsucc (Lvar 1)))
(PAsucc (PAplus (PAnat i) (Lvar 1))))
1 (PAnat j)) as felim.
rewrite Subst_eq, SubstTerm_PAsucc, SubstTerm_PAplus in felim.
rewrite SubstTerm_PAplus, SubstTerm_PAnat in felim.
rewrite SubstTerm_PAsucc, SubstTerm_var in felim.
simpl in felim. apply felim; clear felim.
2: apply IsLterm_PAnat.
2: apply IsFreeForSubst_rel2.
clear IHj j.
pose proof (LforallElim IsWeakHeytingAxiom
(Lforall 1 (Leq (PAplus (Lvar 0) (PAsucc (Lvar 1)))
(PAsucc (PAplus (Lvar 0) (Lvar 1)))))
0 (PAnat i) IsProvedAx5
(IsLterm_PAnat _)) as felim.
rewrite Subst_forall, Subst_eq in felim; simpl in felim.
rewrite SubstTerm_PAsucc, SubstTerm_PAplus in felim.
rewrite SubstTerm_PAsucc, SubstTerm_var, SubstTerm_var in felim.
simpl in felim.
rewrite SubstTerm_PAplus, SubstTerm_var, SubstTerm_var in felim.
simpl in felim.
apply felim.
rewrite IsFreeForSubst_forall.
unfold Leq.
rewrite IsFreeForSubst_rel2.
rewrite VarOccursFreeInFormula_rel2.
unfold PAplus, PAsucc.
rewrite VarOccursInTerm_op2, VarOccursInTerm_op1.
rewrite VarOccursInTerm_op1, VarOccursInTerm_op2.
rewrite VarOccursInTerm_var, VarOccursInTerm_var.
rewrite PAnat_closed. reflexivity.
Qed.
(* Closed terms are proved equal to closed terms with the successor symbol only. *)
Lemma PAmult_normalize : forall i j,
IsProved IsWeakHeytingAxiom (Leq (PAmult (PAnat i) (PAnat j)) (PAnat (i * j))).
Proof.
induction j.
rewrite Nat.mul_0_r. apply PAmult_zero.
apply IsLterm_PAnat.
apply (LeqTrans _ _ (PAplus (PAmult (PAnat i) (PAnat j)) (PAnat i))).
pose proof (LforallElim IsWeakHeytingAxiom
(Lforall 1 (Leq (PAmult (Lvar 0) (PAsucc (Lvar 1)))
(PAplus (PAmult (Lvar 0) (Lvar 1)) (Lvar 0))))
0 (PAnat i)) as felim.
rewrite Subst_forall in felim. simpl in felim.
apply (LforallElim IsWeakHeytingAxiom _ 1 (PAnat j)) in felim.
rewrite Subst_eq, Subst_eq in felim.
rewrite SubstTerm_PAmult, SubstTerm_PAplus in felim.
rewrite SubstTerm_PAmult, SubstTerm_var in felim. simpl in felim.
rewrite SubstTerm_PAmult, SubstTerm_var in felim. simpl in felim.
rewrite SubstTerm_PAplus, SubstTerm_var in felim. simpl in felim.
rewrite SubstTerm_PAsucc, SubstTerm_var in felim. simpl in felim.
rewrite SubstTerm_PAsucc, SubstTerm_var in felim. simpl in felim.
rewrite SubstTerm_PAmult, SubstTerm_var in felim. simpl in felim.
rewrite SubstTerm_PAnat in felim. exact felim. clear felim.
exact IsProvedAx7.
apply IsLterm_PAnat.
apply IsFreeForSubst_PAnat.
rewrite IsLproposition_forall, IsLproposition_eq.
unfold PAmult, PAplus, PAsucc.
rewrite IsLterm_op2, IsLterm_op2, IsLterm_op2, IsLterm_op1.
rewrite IsLterm_var, IsLterm_var. reflexivity.
apply IsLterm_PAnat.
apply IsFreeForSubst_PAnat.
apply SubstIsLproposition.
rewrite IsLproposition_eq.
unfold PAmult, PAplus, PAsucc.
rewrite IsLterm_op2, IsLterm_op2, IsLterm_op2, IsLterm_op1.
rewrite IsLterm_var, IsLterm_var. reflexivity.
apply IsLterm_PAnat.
apply (LeqTrans _ _ (PAplus (PAnat (i*j)) (PAnat i))).
2: rewrite Nat.mul_succ_r; apply PAplus_normalize.
apply LeqElim_op2.
exact IHj. apply LeqRefl, IsLterm_PAnat.
Qed.
Lemma PAle_normalize : forall i j,
i <= j -> IsProved IsWeakHeytingAxiom (PAle (PAnat i) (PAnat j)).
Proof.
intros i j ilej.
pose proof (IsProvedLe (PAnat i) (PAnat j)) as H.
apply LandElim2 in H.
apply (LimpliesElim _ _ _ H). clear H.
apply (LexistsIntro _ _ _ (PAnat (j-i))).
apply IsLterm_PAnat.
unfold PAplus. rewrite IsLproposition_eq, IsLterm_op2, IsLterm_var.
rewrite IsLterm_PAnat, IsLterm_PAnat. reflexivity.
apply IsFreeForSubst_PAnat.
unfold PAplus.
rewrite IsLproposition_eq, IsLterm_op2, IsLterm_var, IsLterm_PAnat, IsLterm_PAnat.
reflexivity.
rewrite Subst_eq, SubstTerm_PAplus.
rewrite SubstTerm_var, SubstTerm_PAnat, SubstTerm_PAnat. simpl.
apply (LeqTrans _ _ (PAnat ((j-i) + i))).
apply PAplus_normalize.
rewrite Nat.sub_add. apply LeqRefl.
apply IsLterm_PAnat. exact ilej.
apply IsLterm_PAnat. apply IsLterm_PAnat.
apply PAnat_closed. apply PAnat_closed.
Qed.
Lemma PAle_zero : forall t,
IsLterm t = true
-> IsProved IsWeakHeytingAxiom
(Limplies (PAle t PAzero) (Leq t PAzero)).
Proof.
assert (IsProved IsWeakHeytingAxiom
(Limplies (PAle (Lvar 3) PAzero) (Leq (Lvar 3) PAzero))).
pose proof (IsProvedLe (Lvar 3) PAzero (IsLterm_var 3) (IsLterm_PAnat 0)) as H.
apply LandElim1 in H.
apply (LimpliesTrans _ _ _ _ H). clear H.
apply LexistsElim_impl.