Last active
October 22, 2024 19:16
-
-
Save Iainmon/d6cd3b84a924c317291e07231ee65ff6 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Unicode.Utf8. | |
Require Import Psatz. | |
Require Import Coq.Arith.Arith. | |
Require Import Coq.Init.Nat. (* needed? it seems no, with next line. *) | |
Import Nat. | |
Open Scope nat_scope. | |
Check add_0_r. | |
Axiom give_up : forall (P : Prop), P. | |
Ltac give_up := apply give_up. | |
Goal | |
forall a b c d, | |
a <= b -> | |
c <= d -> | |
a + c <= b + d. | |
Proof. | |
intros a b c d. | |
lia. | |
Qed. | |
Goal forall (n m : nat), | |
{n = m} + {n <> m}. | |
Proof. | |
induction n. | |
+ intros m. destruct m. | |
- left. reflexivity. | |
- right. discriminate. | |
+ destruct m. | |
- right. discriminate. | |
- pose proof (IHn m) as H1. | |
inversion H1 as [H_eq | H_neq]. | |
* left. rewrite H_eq. reflexivity. | |
* right. auto. | |
Qed. | |
Check Nat.divide. | |
(* Inductive com_div : nat -> nat -> nat -> Prop := | |
| com_div_both : forall (a b d : nat), *) | |
Definition common_div (a b d : nat) := (d | a) /\ (d | b). | |
Inductive greatest_common_div : nat -> nat -> nat -> Prop := | |
| divs_all_div : | |
forall a b d, | |
common_div a b d -> | |
(forall d', common_div a b d' -> (d' | d)) -> | |
greatest_common_div a b d. | |
Inductive nat_set : (nat -> Prop) -> Prop := | |
| dec_nat_set : forall (f : nat -> Prop), | |
(forall n, f n \/ ~ f n) -> nat_set f. | |
Definition nonempty (f : nat -> Prop) := exists n, f n. | |
Lemma no_name_lemma_1: | |
forall f, | |
nat_set f -> | |
nonempty f -> | |
forall n, f n -> | |
forall m, | |
m <= n -> f m \/ ~ f m. | |
Proof. | |
intros f. | |
intros Hf_ns. | |
destruct Hf_ns as [f Hf_dec]. | |
intros Hf_nem. | |
unfold nonempty in Hf_nem. | |
intros n. | |
intros Hn. | |
intros m. | |
intros Hmn. | |
apply Hf_dec. | |
Qed. | |
Definition is_min (f : nat -> Prop) := | |
fun n => f n /\ (forall k, k < n -> ~ f k). | |
(* Lemma nat_has_least_element : | |
forall *) | |
Fixpoint pred_elem f (n : nat) : Prop := | |
match n with | |
| 0 => False | |
| S n' => f n' \/ pred_elem f n' | |
end. | |
Fixpoint no_pred_elem f (n : nat) : Prop := | |
match n with | |
| 0 => ~ f n | |
| S n' => (~ f n) /\ no_pred_elem f n' | |
end. | |
Lemma pred_elem_exists : | |
forall f, | |
nat_set f -> | |
forall n, pred_elem f n <-> exists m, f m /\ m < n. | |
Proof. | |
intros f. | |
intros Hf_ns. | |
destruct Hf_ns as [f Hf_dec]. | |
induction n; split. | |
- simpl. contradiction. | |
- intros H2. | |
destruct H2 as [m [H2 H3]]. | |
apply Nat.nlt_0_r in H3. | |
assumption. | |
- intros H1. | |
simpl in H1. | |
destruct H1 as [H1 | H2]. | |
+ exists n. auto. | |
+ apply IHn in H2. | |
destruct H2 as [m [H1 H2]]. | |
exists m. | |
auto. | |
- intros H1. | |
destruct H1 as [m [H1 H2]]. | |
simpl. | |
pose proof (Nat.eq_dec n m) as H3. | |
destruct H3 as [Heq | Hneq]. | |
+ left. rewrite Heq. assumption. | |
+ right. assert (m < n). { lia. } | |
apply IHn. | |
exists m. auto. | |
Qed. | |
Lemma pred_elem_dec : | |
forall f, | |
nat_set f -> | |
forall n, | |
pred_elem f n \/ ~ pred_elem f n. | |
Proof. | |
intros f. | |
intros Hf_ns. | |
destruct Hf_ns as [f Hf_dec]. | |
induction n. | |
- right. simpl. auto. | |
- simpl. destruct IHn as [H1 | H2]. | |
+ left. auto. | |
+ destruct (Hf_dec n) as [H3 | H4]. | |
* left. auto. | |
* right. | |
intros H. destruct H as [H5 | H6]. | |
-- apply H4. assumption. | |
-- apply H2. assumption. | |
Qed. | |
Lemma no_name_lemma_3 : | |
forall f, | |
nat_set f -> | |
nonempty f -> | |
exists n, ~ pred_elem f n /\ pred_elem f (S n). | |
Proof. | |
intros f. | |
intros Hf_ns. | |
destruct Hf_ns as [f Hf_dec]. | |
intros Hf_nem. | |
unfold nonempty in Hf_nem. | |
pose proof (pred_elem_exists f (dec_nat_set f Hf_dec)) as H1. | |
destruct Hf_nem as [k Hk]. | |
induction k. | |
- exists 0. simpl. split. | |
+ auto. | |
+ left. assumption. | |
- pose proof (Hf_dec k) as H2. | |
pose proof (pred_elem_dec f (dec_nat_set f Hf_dec)) as H3. | |
(***) | |
destruct H2 as [Hfk | Hnfk]. | |
+ apply IHk in Hfk. assumption. | |
+ (*pose proof (H3 k) as H4. | |
pose proof (H3 (S k)) as H5. | |
pose proof (H3 (S (S k))) as H6.*) | |
(* pose proof (H1 k) as H6. *) | |
simpl. | |
assert ((exists n, ~ pred_elem f n /\ f n) -> (exists n, ~ pred_elem f n /\ pred_elem f (S n))). | |
{ simpl. intros H. destruct H as [x [Hx1 Hx2]]. exists x. split; try assumption. left. assumption. } | |
apply H. (*clear H.*) | |
pose proof (H3 (S k)) as H4. | |
destruct H4 as [H4 | H4]. | |
* apply H1 in H4 as H5. | |
destruct H5 as [m [H5 H6]]. | |
pose proof (H3 m) as H7. | |
admit. | |
* | |
Lemma no_name_lemma_2 : | |
forall f, | |
nat_set f -> | |
nonempty f -> | |
forall n, | |
f n -> | |
pred_elem f n <-> exists m, m < n /\ f m. | |
Proof. | |
intros f. | |
intros Hf_ns. | |
destruct Hf_ns as [f Hf_dec]. | |
intros Hf_nem. | |
unfold nonempty in Hf_nem. | |
induction n; intros H1; split. | |
- simpl. contradiction. | |
- intros H2. | |
destruct H2 as [m [H2 H3]]. | |
apply Nat.nlt_0_r in H2. | |
assumption. | |
- generalize dependent n. | |
intros H2. | |
destruct H2 as [H2 | H2]. | |
Admitted. | |
Lemma least_element : | |
forall f, | |
nat_set f -> | |
nonempty f -> | |
exists n, f n /\ forall m, f m -> n <= m. | |
Proof. | |
intros f. | |
intros Hf_ns. | |
destruct Hf_ns as [f Hf_dec]. | |
intros Hf_nem. | |
unfold nonempty in Hf_nem. | |
pose proof (no_name_lemma_1 f (dec_nat_set f Hf_dec) Hf_nem) as H2. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment