Skip to content

Instantly share code, notes, and snippets.

@vit0rr

vit0rr/a.v

Created August 13, 2023 01:42
Show Gist options
  • Save vit0rr/c26e19203ecb0232c92e772de40b5803 to your computer and use it in GitHub Desktop.
Save vit0rr/c26e19203ecb0232c92e772de40b5803 to your computer and use it in GitHub Desktop.
Download ZIP
Proof in Coq that natural numbers are infinity
Raw
a.v
Theorem plus_1_n : forall n : nat, n + 1 = S n /\ S n > n.
Proof.
intros n.
split.
- induction n as [| n' IHn'].
+ simpl. reflexivity.
+ simpl. rewrite <- IHn'. reflexivity.
- induction n as [| n' IHn'].
+ simpl. apply le_n.
+ simpl. apply le_n_S. apply IHn'.
Qed.
Print plus_1_n.
> plus_1_n = fun n : nat => conj (nat_ind (fun n0 : nat => n0 + 1 = S n0) (eq_refl : 0 + 1 = 1) (fun (n' : nat) (IHn' : n' + 1 = S n') => eq_ind (n' + 1) (fun n0 : nat => S (n' + 1) = S n0) eq_refl (S n') IHn' : S n' + 1 = S (S n')) n) (nat_ind (fun n0 : nat => S n0 > n0) (le_n 1 : 1 > 0) (fun (n' : nat) (IHn' : S n' > n') => le_n_S (S n') (S n') IHn' : S (S n') > S n') n)
: forall n : nat, n + 1 = S n /\ S n > n
Theorem plus_1_natural : forall n : nat, 1 + n = S n /\ S n > n.
Proof.
intros n.
split.
- reflexivity.
- apply le_n_S. apply le_n.
Qed.
Print plus_1_natural.
> plus_1_natural = fun n : nat => conj eq_refl (le_n_S n n (le_n n))
: forall n : nat, 1 + n = S n /\ S n > n
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment