Peano.v 14.5 KB
Newer Older
1

2
3
(** * The Theory of Peano Arithmetic and its Coq model *)

4
(** The NatDed development, Pierre Letouzey, Samuel Ben Hamou, 2019-2020.
5
6
    This file is released under the CC0 License, see the LICENSE file *)

7
Require Import Defs NameProofs Mix Meta Toolbox.
8
Require Import Wellformed Theories Nary PreModels Models.
9
10
Import ListNotations.
Local Open Scope bool_scope.
11
Local Open Scope string_scope.
12
13
Local Open Scope eqb_scope.

14
15
16
17
(** The Peano axioms *)

Definition PeanoSign := Finite.to_infinite peano_sign.

18
19
Notation Zero := (Fun "O" []).
Notation Succ x := (Fun "S" [x]).
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

Notation "x = y" := (Pred "=" [x;y]) : formula_scope.
Notation "x + y" := (Fun "+" [x;y]) : formula_scope.
Notation "x * y" := (Fun "*" [x;y]) : formula_scope.

Module PeanoAx.
Local Open Scope formula_scope.

Definition ax1 :=  (#0 = #0).
Definition ax2 := ∀∀ (#1 = #0 -> #0 = #1).
Definition ax3 := ∀∀∀ (#2 = #1 /\ #1 = #0 -> #2 = #0).

Definition ax4 := ∀∀ (#1 = #0 -> Succ (#1) = Succ (#0)).
Definition ax5 := ∀∀∀ (#2 = #1 -> #2 + #0 = #1 + #0).
Definition ax6 := ∀∀∀ (#1 = #0 -> #2 + #1 = #2 + #0).
Definition ax7 := ∀∀∀ (#2 = #1 -> #2 * #0 = #1 * #0).
Definition ax8 := ∀∀∀ (#1 = #0 -> #2 * #1 = #2 * #0).

Definition ax9 :=  (Zero + #0 = #0).
Definition ax10 := ∀∀ (Succ(#1) + #0 = Succ(#1 + #0)).
40
Definition ax11 :=  (Zero * #0 = Zero).
41
42
43
44
45
46
Definition ax12 := ∀∀ (Succ(#1) * #0 = (#1 * #0) + #0).

Definition ax13 := ∀∀ (Succ(#1) = Succ(#0) -> #1 = #0).
Definition ax14 :=  ~(Succ(#0) = Zero).

Definition axioms_list :=
47
 [ ax1; ax2; ax3; ax4; ax5; ax6; ax7; ax8;
48
49
    ax9; ax10; ax11; ax12; ax13; ax14 ].

50
51
52
(** Beware, [bsubst] is ok below for turning [#0] into [Succ #0], but
    only since it contains now a [lift] of substituted terms inside
    quantifiers.
53
54
55
    And the unconventional [] before [A[0]] is to get the right
    bounded vars (Hack !). *)

56
57
58
Definition induction_schema A_x :=
  let A_0 := bsubst 0 Zero A_x in
  let A_Sx := bsubst 0 (Succ(#0)) A_x in
59
  nForall
60
61
    (Nat.pred (level A_x))
    ((( A_0) /\ ( (A_x -> A_Sx))) ->  A_x).
62
63
64
65
66
67

Local Close Scope formula_scope.

Definition IsAx A :=
  List.In A axioms_list \/
  exists B, A = induction_schema B /\
68
            check PeanoSign B = true /\
69
70
            FClosed B.

71
Lemma WCAx A : IsAx A -> WC PeanoSign A.
72
73
Proof.
 intros [ IN | (B & -> & HB & HB')].
74
 - apply wc_iff. revert A IN. now apply forallb_forall.
75
76
 - repeat split; unfold induction_schema; cbn.
   + rewrite nForall_check. cbn.
77
     rewrite !check_bsubst, HB; auto.
78
79
80
   + red. rewrite nForall_level. cbn.
     assert (level (bsubst 0 Zero B) <= level B).
     { apply level_bsubst'. auto. }
81
82
     assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B).
     { apply level_bsubst'. auto. }
83
     omega with *.
84
85
   + apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
     cbn. now rewrite !fclosed_bsubst, HB'.
86
87
88
89
Qed.

End PeanoAx.

90
91
Local Open Scope formula_scope.

92
Definition PeanoTheory :=
93
 {| sign := PeanoSign;
94
    IsAxiom := PeanoAx.IsAx;
95
    WCAxiom := PeanoAx.WCAx |}.
96

97
(** Useful lemmas so as to be able to write proofs that take less than 1000 lines. *)
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
98

99
100
Import PeanoAx.

101
102
103
Lemma Symmetry :
  forall logic A B Γ, BClosed A -> In ax2 Γ -> Pr logic (Γ  A = B) ->
                      Pr logic (Γ  B = A).
104
105
106
107
Proof.
  intros.
  apply R_Imp_e with (A := A = B); [ | assumption ].
  assert (AX2 : Pr logic (Γ  ax2)).
108
  { apply R_Ax. exact H0. }
109
  unfold ax2 in AX2.
110
111
  apply R_All_e with (t := A) in AX2.
  apply R_All_e with (t := B) in AX2.
112
  cbn in AX2.
Pierre Letouzey's avatar
Pierre Letouzey committed
113
114
  assert (bsubst 0 B (lift 0 A) = A).
  { assert (lift 0 A = A). { apply lift_nop. exact H. } rewrite H2. apply bclosed_bsubst_id. exact H. }
115
  rewrite H2 in AX2.
116
117
118
  exact AX2.
Qed.

119
120
121
Lemma Transitivity :
  forall logic A B C Γ, BClosed A -> BClosed B -> In ax3 Γ ->
                        Pr logic (Γ  A = B) -> Pr logic (Γ  B = C) -> Pr logic (Γ  A = C).
122
123
124
125
Proof.
  intros.
  apply R_Imp_e with (A := A = B /\ B = C); [ | apply R_And_i; assumption ].
  assert (AX3 : Pr logic (Γ  ax3)).
126
  { apply R_Ax. exact H1. }
127
  unfold ax3 in AX3.
128
129
130
  apply R_All_e with (t := A) in AX3.
  apply R_All_e with (t := B) in AX3.
  apply R_All_e with (t := C) in AX3.
131
  cbn in AX3.
Pierre Letouzey's avatar
Pierre Letouzey committed
132
133
  assert (bsubst 0 C (lift 0 B) = B).
  { assert (lift 0 B = B). {apply lift_nop. assumption. } rewrite H4. apply bclosed_bsubst_id. assumption. }
134
  rewrite H4 in AX3.
Pierre Letouzey's avatar
Pierre Letouzey committed
135
136
137
  assert (bsubst 0 C (bsubst 1 (lift 0 B) (lift 0 (lift 0 A))) = A).
  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H5. rewrite H5.
    assert (lift 0 B = B). { apply lift_nop. assumption. } rewrite H6.
138
    assert (bsubst 1 B A = A). { apply bclosed_bsubst_id. assumption. } rewrite H7.
139
    apply bclosed_bsubst_id. assumption. }
140
  rewrite H5 in AX3.
141
142
143
  assumption.
Qed.

144
145
146
Lemma Hereditarity :
  forall logic A B Γ, BClosed A -> In ax4 Γ -> Pr logic (Γ  A = B) ->
                      Pr logic (Γ  Succ A = Succ B).
147
148
149
150
151
152
Proof.
  intros.
  apply R_Imp_e with (A := A = B); [ | assumption ].
  assert (AX4 : Pr logic (Γ  ax4)).
  { apply R_Ax. assumption. }
  unfold ax4 in AX4.
153
154
  apply R_All_e with (t := A) in AX4.
  apply R_All_e with (t := B) in AX4.
155
  cbn in AX4.
Pierre Letouzey's avatar
Pierre Letouzey committed
156
157
  assert (bsubst 0 B (lift 0 A) = A).
  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H2.
158
    apply bclosed_bsubst_id. assumption. }
159
  rewrite H2 in AX4.
160
161
162
  assumption.
Qed.

163
164
165
Lemma AntiHereditarity :
  forall logic A B Γ, BClosed A -> In ax13 Γ -> Pr logic (Γ  Succ A = Succ B) ->
                      Pr logic (Γ  A = B).
166
167
168
169
170
171
Proof.
  intros.
  apply R_Imp_e with (A := Succ A = Succ B); [ | assumption ].
  assert (AX13 : Pr logic (Γ  ax13)).
  { apply R_Ax. assumption. }
  unfold ax13 in AX13.
172
173
  apply R_All_e with (t := A) in AX13.
  apply R_All_e with (t := B) in AX13.
174
  cbn in AX13.
Pierre Letouzey's avatar
Pierre Letouzey committed
175
176
  assert (bsubst 0 B (lift 0 A) = A).
  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H2.
177
    apply bclosed_bsubst_id. assumption. }
178
  rewrite H2 in AX13.
179
180
181
  assumption.
Qed.

182
183
184
185
186
187
188
189
190
191
192
193
194
Lemma IsAx_adhoc form :
  check PeanoSign form = true ->
  FClosed form ->
  Forall IsAx (induction_schema form ::axioms_list).
Proof.
  intros.
  apply Forall_forall.
  intros x Hx.
  destruct Hx.
  + simpl. unfold IsAx. right. exists form. split; [ auto | split; [ auto | auto ]].
  + simpl. unfold IsAx. left. assumption.
Qed.

195
Lemma rec0_rule l Γ A_x :
196
  BClosed ( A_x) ->
197
198
199
200
  In (induction_schema A_x) Γ ->
  Pr l (Γ  bsubst 0 Zero A_x) ->
  Pr l (Γ   (A_x -> bsubst 0 (Succ(#0)) A_x)) ->
  Pr l (Γ   A_x).
201
202
203
204
205
206
207
208
209
210
211
212
Proof.
  intros.
  eapply R_Imp_e.
  + apply R_Ax.
    unfold induction_schema in H0.
    unfold BClosed in H.
    cbn in H.
    rewrite H in H0.
    cbn in H0.
    apply H0.
  + simpl.
    apply R_And_i; cbn.
213
    * set (v := fresh (fvars (Γ   bsubst 0 Zero A_x)%form)).
214
215
216
217
      apply R_All_i with (x:=v).
      apply fresh_ok.
      rewrite form_level_bsubst_id.
      - assumption.
218
      - now apply level_bsubst, pred_0.
219
220
221
222
223
    * assumption.
Qed.

(* And tactics to make the proofs look like natural deduction proofs. *)

Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
224
225
226
227
228
229
230
Ltac reIff :=
  match goal with
  | |- context [ ((?A -> ?B) /\ _ )%form ] => fold (Iff A B); reIff
  | H : context [ ((?A -> ?B) /\ _ )%form ] |- _ => fold (Iff A B) in H; reIff
  | _ => idtac
  end.

231
Ltac calc :=
232
  match goal with
233
234
235
  | |- BClosed _ => reflexivity
  | |- In _ _ => rewrite <- list_mem_in; reflexivity
  | |- ~Names.In _ _ => rewrite<- Names.mem_spec; now compute
236
  | _ => trivial
237
  end.
238

239
240
241
Ltac inst H l :=
  match l with
  | [] => idtac
242
  | (?u::?l) => apply R_All_e with (t := u) in H; inst H l
243
  end.
244

245
246
Ltac axiom ax name :=
  match goal with
247
248
249
    | |- Pr ?l (?ctx  _) =>
      assert (name : Pr l (ctx  ax)); [ apply R_Ax; calc | ];
      try unfold ax in name
250
  end.
251

252
253
Ltac inst_axiom ax l :=
 let H := fresh in
254
 axiom ax H; inst H l; try easy.
255

Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
256
Ltac app_R_All_i t v := apply R_All_i with (x := t); calc; cbn; set (v := FVar t); reIff.
257
Ltac eapp_R_All_i := eapply R_All_i; calc.
258

259
Ltac sym := apply Symmetry; calc.
260

261
Ltac ahered := apply Hereditarity; calc.
262

263
Ltac hered := apply AntiHereditarity; calc.
264

265
266
Ltac trans b := apply Transitivity with (B := b); calc.

267
Ltac thm := unfold IsTheorem; split; [ now apply wc_iff | ].
268

269
270
271
272
273
274
Ltac parse term :=
  match term with
  | (_ -> ?queue)%form => parse queue
  | ( ?formula)%form => formula
  end.

275
Ltac rec :=
276
  match goal with
277
278
  | |- exists axs, (Forall (IsAxiom PeanoTheory) axs /\ Pr ?l (axs  ?A))%type => 
    let form := parse A in  
279
280
    exists (induction_schema form :: axioms_list); set (rec := induction_schema form); set (Γ := rec :: axioms_list); split;
      [ apply IsAx_adhoc; auto |
281
        repeat apply R_Imp_i;
282
        apply rec0_rule; calc ]; cbn
283
    (* | _ => idtac *)
284
  end.
285

286
            
287
288
(** Some basic proofs in Peano arithmetics. *)

289
Lemma ZeroRight :
290
  IsTheorem J PeanoTheory
291
            ( (#0 = #0 + Zero)).
292
293
294
Proof.
 thm.
 rec.
295
296
297
298
 + sym.
   inst_axiom ax9 [Zero].
 + app_R_All_i "y" y.
   apply R_Imp_i. set (H1 := _ = _).
299
   sym.
300
301
   trans (Succ (y + Zero)).
   - inst_axiom ax10 [y; Zero].
302
303
304
305
   - ahered.
     sym.
     apply R_Ax.
     apply in_eq.
306
Qed.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
307

308
Lemma SuccRight : IsTheorem J PeanoTheory (∀∀ (Succ(#1 + #0) = #1 + Succ(#0))).
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
309
Proof.
310
311
  thm.
  rec.
312
  + app_R_All_i "y" y.
313
    sym.
314
315
    trans (Succ y).
    - inst_axiom ax9 [Succ y].
316
317
    - ahered.
      sym.
318
319
      inst_axiom ax9 [y].
  + app_R_All_i "x" x.
320
    apply R_Imp_i.
321
    app_R_All_i "y" y. fold x.
322
    set (hyp :=  Succ _ = _).
323
    trans (Succ (Succ (x + y))).
324
    - ahered.
325
326
      inst_axiom ax10 [x; y].
    - trans (Succ (x + Succ y)).
327
      * ahered.
328
329
330
        inst_axiom hyp [y].
      * sym.
        inst_axiom ax10 [x; Succ y].
331
Qed.
332

333
Lemma Comm :
334
  IsTheorem J PeanoTheory
335
336
            (( #0 = #0 + Zero) -> (∀∀ Succ(#1 + #0) = #1 + Succ(#0)) ->
               (∀∀ #0 + #1 = #1 + #0)).
337
Proof.
338
  thm.
339
  rec; set (Γ' := _ :: _ :: Γ).
340
341
  + app_R_All_i "x" x.
    trans x.
342
    - sym.
343
      assert (Pr J (Γ'   # 0 = # 0 + Zero)). { apply R_Ax. calc. }
344
      apply R_All_e with (t := x) in H; auto.
345
    - sym.
346
347
      inst_axiom ax9 [x].
  + app_R_All_i "y" y.
348
    apply R_Imp_i.
349
350
    app_R_All_i "x" x.
    trans (Succ (x + y)).
351
    - sym.
352
      assert (Pr J (( #0 + y = y + #0) :: Γ'    Succ (#1 + #0) = #1 + Succ (#0))). { apply R_Ax. calc. }
353
354
355
      apply R_All_e with (t := x) in H; auto.
      apply R_All_e with (t := y) in H; auto.
    - trans (Succ (y + x)).
356
      * ahered.
357
        assert (Pr J (( #0 + y = y + #0) :: Γ'   #0 + y = y + #0)). { apply R_Ax. apply in_eq. }
358
        apply R_All_e with (t := x) in H; auto.
359
      * sym.
360
        inst_axiom ax10 [y; x].
361
Qed.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
362

363
Lemma Commutativity : IsTheorem J PeanoTheory (∀∀ #0 + #1 = #1 + #0).
364
365
366
367
368
369
370
Proof.
  apply ModusPonens with (A := (∀∀ Succ(#1 + #0) = #1 + Succ(#0))).
  + apply ModusPonens with (A :=  #0 = #0 + Zero).
    * apply Comm.
    * apply ZeroRight.
  + apply SuccRight.
Qed.
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
Lemma Predecessor : IsTheorem J PeanoTheory ( (~#0=Zero ->  Succ(#0) = #1)).
Proof.
 thm.
 rec.
 - apply R_Imp_i.
   apply R_Fa_e.
   eapply R_Not_e; [ | apply R'_Ax].
   now inst_axiom ax1 [Zero].
 - app_R_All_i "x" x.
   apply R_Imp_i.
   apply R_Imp_i.
   apply R_Ex_i with x. now inst_axiom ax1 [Succ(x)].
Qed.

Lemma Middle : IsTheorem J PeanoTheory (∀∃ (#0+#0 = #1 \/ Succ(#0+#0) = #1)).
Proof.
 eapply ModusPonens; [ | exact SuccRight].
 thm.
 set (SR :=  _).
 rec.
 - apply R_Ex_i with Zero. cbn.
   apply R_Or_i1. now inst_axiom ax9 [Zero].
 - app_R_All_i "x" x.
   apply R_Imp_i.
   eapply R'_Ex_e with "y". calc. cbn. set (y := FVar "y") in *.
   fold x.
   apply R'_Or_e.
   + apply R_Ex_i with y. cbn. fold x; fold y.
     apply R_Or_i2. ahered. apply R'_Ax.
   + apply R_Ex_i with (Succ y). cbn. fold x; fold y.
     apply R_Or_i1.
     trans (Succ (y+Succ(y))).
     * now inst_axiom ax10 [y;Succ(y)].
     * ahered.
       trans (Succ (y+y)).
       { sym. inst_axiom SR [y;y]. }
       { apply R'_Ax. }
Qed.

411
412
(** A Coq model of this Peano theory, based on the [nat] type *)

413
Definition PeanoFuns : string -> optnfun nat nat :=
414
  fun f =>
415
416
417
418
419
  if f =? "O" then NFun 0 0
  else if f =? "S" then NFun 1 S
  else if f =? "+" then NFun 2 Nat.add
  else if f =? "*" then NFun 2 Nat.mul
  else Nop.
420

421
Definition PeanoPreds : string -> optnfun nat Prop :=
422
  fun p =>
423
424
  if p =? "=" then NFun 2 Logic.eq
  else Nop.
425
426
427
428
429

Lemma PeanoFuns_ok s :
 funsymbs PeanoSign s = get_arity (PeanoFuns s).
Proof.
 unfold PeanoSign, peano_sign, PeanoFuns. simpl.
430
 repeat (case eqbspec; auto); congruence.
431
432
433
434
435
436
Qed.

Lemma PeanoPreds_ok s :
 predsymbs PeanoSign s = get_arity (PeanoPreds s).
Proof.
 unfold PeanoSign, peano_sign, PeanoPreds. simpl.
437
 repeat (case eqbspec; auto); congruence.
438
439
440
441
442
443
444
445
446
447
Qed.

Definition PeanoPreModel : PreModel nat PeanoTheory :=
 {| someone := 0;
    funs := PeanoFuns;
    preds := PeanoPreds;
    funsOk := PeanoFuns_ok;
    predsOk := PeanoPreds_ok |}.

Lemma PeanoAxOk A :
448
  IsAxiom PeanoTheory A -> interp PeanoPreModel A.
449
450
451
Proof.
 unfold PeanoTheory. simpl.
 unfold PeanoAx.IsAx.
452
 intros [IN|(B & -> & CK & CL)] G.
453
 - compute in IN. intuition; subst; cbn; intros; subst; omega.
454
 - unfold PeanoAx.induction_schema.
455
456
457
458
459
460
   apply interp_nforall.
   intros stk Len. rewrite app_nil_r. cbn.
   intros (Base,Step).
   (* The Peano induction emulated by a Coq induction :-) *)
   induction m.
   + specialize (Base 0).
461
     apply -> finterp_bsubst_gen in Base; simpl; eauto.
462
   + apply Step in IHm.
463
     apply -> finterp_bsubst_gen in IHm; simpl; eauto.
464
465
466
467
468
469
     now intros [|k].
Qed.

Definition PeanoModel : Model nat PeanoTheory :=
 {| pre := PeanoPreModel;
    AxOk := PeanoAxOk |}.
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

(** Essais de tactiques faisant de l'unification *)

Definition first_success (f:term->term->option term) :=
 fix first_success l l' :=
 match l, l' with
 | t::l, t'::l' =>
   match f t t' with
   | None => first_success l l'
   | r => r
   end
 | _, _ => None
 end.

Fixpoint get_inst_term n t t' :=
  match t, t' with
  | BVar k, _ => if k =? n then Some t' else None
  | Fun _ l, Fun _ l' => first_success (get_inst_term n) l l'
  | _, _ => None
  end.

Fixpoint get_inst n f f' :=
  match f, f' with
  | Pred _ l, Pred _ l' => first_success (get_inst_term n) l l'
  | Not f, Not f' => get_inst n f f'
  | Op _ f1 f2, Op _ f1' f2' =>
    match get_inst n f1 f1' with
    | None => get_inst n f2 f2'
    | r => r
    end
  | Quant _ f, f' => get_inst (S n) f f'
  | _, _ => None
  end.

Ltac autoinst H :=
  match type of H with
  | Pr _ (_   ?f) =>
    match goal with
    | |- Pr _ (_  ?f') =>
      let r := eval compute in (get_inst 0 f f') in
      match r with
      | Some ?u => apply R_All_e with (t := u) in H;
                   [cbn in H; autoinst H | calc]
      end
    end
  | _ => idtac
  end.

Ltac autoinstax ax := let H := fresh in axiom ax H; autoinst H; exact H.