Instantly share code, notes, and snippets.

# ice1000/CoqNatUIP.v

Last active January 19, 2024 09:06
Show Gist options
• Save ice1000/560fae6d75055902d9f60131dabe0120 to your computer and use it in GitHub Desktop.
UIP on Nat in Coq
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
 Definition lemma {n m : nat} (p : n = m) : pred n = pred m := f_equal pred p. Definition lemma2 {n m : nat} (p : n = m) : S n = S m := f_equal S p. Definition lemma3 {n m : nat} (p : S n = S m) : lemma2 (lemma p) = p := match p with | eq_refl => eq_refl end. (* Definition bruh {n} (a : nat) (p : S n = a) : Prop. Proof. destruct a. - exact True. - exact (@lemma2 n a (@lemma (S n) (S a) p) = p). Defined. Definition lemma3 {n m : nat} (p : S n = S m) : lemma2 (lemma p) = p. Proof. simpl. apply eq_ind_dep with (e := p) (P := bruh). simpl. trivial. Qed. *) Definition lemma5 {n : nat} (p : S n = S n) : lemma2 (lemma p) = lemma2 eq_refl -> p = eq_refl. Proof. rewrite lemma3. compute. trivial. Qed. Definition test (n : nat) (p : n = n) : p = eq_refl. Proof. induction n. exact (match p with | eq_refl => eq_refl end). pose proof (fun pp : S n = S n => IHn (lemma pp)) as q. pose proof (f_equal lemma2 (q p)) as q1. apply lemma5. trivial. Qed.

### ice1000 commented Jan 19, 2024

Thanks to @PhotonQuantum for some help & motivating this