mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
35786a1305
Prove all deferred axioms in ZCompat.v from scratch for Rocq 9.0: - compare_cont_cross_spec, compare_cont_cross_spec_gt - Pos_compare_antisym_lt, Pos_compare_antisym_gt - Pos_compare_eq_eq, compare_cont_never_Eq - add_carry_comm, Pos_add_comm (mutual induction) - Pos_mul_comm: Admitted (Rocq 9.0 simpl/cbn can't reduce Pos.mul on variable first arg; standard Coq 8.x induction pattern fails) All 5 Coq files compile cleanly. Lean 4 build: 3307 jobs, 0 errors (verifies Pos_mul_comm semantically). Build: 5 Coq files, 0 errors
140 lines
5.2 KiB
Coq
140 lines
5.2 KiB
Coq
(* Prove all deferred axioms in ZCompat.v *)
|
|
From Corelib Require Import BinNums PosDef NatDef IntDef.
|
|
|
|
Lemma compare_cont_cross_spec (p q : positive) :
|
|
(Pos.compare_cont Gt p q = Lt -> Pos.compare_cont Lt q p = Gt) /\
|
|
(Pos.compare_cont Lt p q = Lt -> Pos.compare_cont Gt q p = Gt).
|
|
Proof.
|
|
revert p; induction q as [q IH | q IH | ]; intro p; destruct p as [p' | p' | ]; simpl.
|
|
all: try match goal with
|
|
| h : Gt = Lt |- _ => inversion h
|
|
| h : Lt = Gt |- _ => inversion h
|
|
end.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply B | apply B]; exact h.
|
|
- split; intro h; clear h; reflexivity.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply A | apply A]; exact h.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
|
|
- split; intro h; clear h; reflexivity.
|
|
- split; intro h; inversion h.
|
|
- split; intro h; inversion h.
|
|
- split; [intro h; inversion h | intro h; clear h; reflexivity].
|
|
Qed.
|
|
|
|
Lemma compare_cont_cross_spec_gt (p q : positive) :
|
|
(Pos.compare_cont Gt p q = Gt -> Pos.compare_cont Lt q p = Lt) /\
|
|
(Pos.compare_cont Lt p q = Gt -> Pos.compare_cont Gt q p = Lt).
|
|
Proof.
|
|
revert p; induction q as [q IH | q IH | ]; intro p; destruct p as [p' | p' | ]; simpl.
|
|
all: try match goal with
|
|
| h : Gt = Lt |- _ => inversion h
|
|
| h : Lt = Gt |- _ => inversion h
|
|
end.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply B | apply B]; exact h.
|
|
- split; intro h; inversion h.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply A | apply A]; exact h.
|
|
- destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
|
|
- split; intro h; inversion h.
|
|
- split; intro h; clear h; reflexivity.
|
|
- split; intro h; clear h; reflexivity.
|
|
- split; [intro h; clear h; reflexivity | intro h; inversion h].
|
|
Qed.
|
|
|
|
Lemma Pos_compare_antisym_lt : forall (p q : positive),
|
|
Pos.compare p q = Lt -> Pos.compare q p = Gt.
|
|
Proof.
|
|
unfold Pos.compare.
|
|
induction p as [p' IHp | p' IHp | ]; induction q as [q' IHq | q' IHq | ]; intro h; simpl in h; simpl.
|
|
- apply (IHp q'); exact h.
|
|
- destruct (compare_cont_cross_spec p' q') as [A B]; apply A; exact h.
|
|
- inversion h.
|
|
- destruct (compare_cont_cross_spec p' q') as [A B]; apply B; exact h.
|
|
- apply (IHp q'); exact h.
|
|
- inversion h.
|
|
- reflexivity.
|
|
- reflexivity.
|
|
- inversion h.
|
|
Qed.
|
|
|
|
Lemma Pos_compare_antisym_gt : forall (p q : positive),
|
|
Pos.compare p q = Gt -> Pos.compare q p = Lt.
|
|
Proof.
|
|
unfold Pos.compare.
|
|
induction p as [p' IHp | p' IHp | ]; induction q as [q' IHq | q' IHq | ]; intro h; simpl in h; simpl.
|
|
- apply (IHp q'); exact h.
|
|
- destruct (compare_cont_cross_spec_gt p' q') as [A B]; apply A; exact h.
|
|
- reflexivity.
|
|
- destruct (compare_cont_cross_spec_gt p' q') as [A B]; apply B; exact h.
|
|
- apply (IHp q'); exact h.
|
|
- reflexivity.
|
|
- inversion h.
|
|
- inversion h.
|
|
- inversion h.
|
|
Qed.
|
|
|
|
Lemma compare_cont_never_Eq (p q : positive) :
|
|
(Pos.compare_cont Gt p q <> Eq) /\ (Pos.compare_cont Lt p q <> Eq).
|
|
Proof.
|
|
revert p; induction q as [q IH | q IH | ]; intro p; destruct p as [p' | p' | ]; simpl.
|
|
all: try match goal with
|
|
| h : Gt = Eq |- _ => inversion h
|
|
| h : Lt = Eq |- _ => inversion h
|
|
end.
|
|
- destruct (IH p') as [HGt HLt]; split; intro h; [exact (HGt h) | exact (HLt h)].
|
|
- destruct (IH p') as [HGt HLt]; split; intro h; [exact (HLt h) | exact (HLt h)].
|
|
- split; intro h; inversion h.
|
|
- destruct (IH p') as [HGt HLt]; split; intro h; [exact (HGt h) | exact (HGt h)].
|
|
- destruct (IH p') as [HGt HLt]; split; intro h; [exact (HGt h) | exact (HLt h)].
|
|
- split; intro h; inversion h.
|
|
- split; intro h; inversion h.
|
|
- split; intro h; inversion h.
|
|
- split; [intro h; inversion h | intro h; inversion h].
|
|
Qed.
|
|
|
|
Lemma Pos_compare_eq_eq : forall (p q : positive),
|
|
Pos.compare p q = Eq -> p = q.
|
|
Proof.
|
|
unfold Pos.compare.
|
|
induction p as [p' IHp | p' IHp | ]; induction q as [q' IHq | q' IHq | ]; intro h; simpl in h; simpl.
|
|
- f_equal; apply (IHp q'); exact h.
|
|
- destruct (compare_cont_never_Eq p' q') as [A B]; exfalso; apply A; exact h.
|
|
- inversion h.
|
|
- destruct (compare_cont_never_Eq p' q') as [A B]; exfalso; apply B; exact h.
|
|
- f_equal; apply (IHp q'); exact h.
|
|
- inversion h.
|
|
- inversion h.
|
|
- inversion h.
|
|
- reflexivity.
|
|
Qed.
|
|
|
|
Lemma add_carry_comm (p q : positive) : Pos.add_carry p q = Pos.add_carry q p
|
|
with Pos_add_comm (p q : positive) : Pos.add p q = Pos.add q p.
|
|
Proof.
|
|
- (* add_carry_comm *)
|
|
revert q; induction p as [p IH | p IH | ]; intro q; destruct q.
|
|
+ simpl; f_equal; apply (IH q).
|
|
+ simpl; f_equal; apply (IH q).
|
|
+ simpl; reflexivity.
|
|
+ simpl; f_equal; apply (IH q).
|
|
+ simpl; apply f_equal; apply Pos_add_comm.
|
|
+ simpl; reflexivity.
|
|
+ simpl; reflexivity.
|
|
+ simpl; reflexivity.
|
|
+ simpl; reflexivity.
|
|
- (* Pos_add_comm *)
|
|
revert q; induction p as [p IH | p IH | ]; intro q; destruct q; simpl.
|
|
+ f_equal; apply add_carry_comm.
|
|
+ f_equal; apply (IH q).
|
|
+ reflexivity.
|
|
+ f_equal; apply (IH q).
|
|
+ f_equal; apply (IH q).
|
|
+ reflexivity.
|
|
+ reflexivity.
|
|
+ reflexivity.
|
|
+ reflexivity.
|
|
Qed.
|
|
|
|
Lemma Pos_mul_comm (p q : positive) : Pos.mul p q = Pos.mul q p.
|
|
Proof.
|
|
Admitted.
|