Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add Compare operational typeclass #79

Merged
merged 3 commits into from
Sep 20, 2021
Merged

add Compare operational typeclass #79

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5bc65eb
add Compare operational typeclass
palmskog Sep 14, 2021
5efcb1d
improve organization, changes based on discussion with Pierre
palmskog Sep 19, 2021
21d43b9
adapt hydras text about Comparable typeclass
palmskog Sep 19, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 7 additions & 6 deletions doc/part-hydras.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1701,24 +1701,25 @@ \section{Ordinal Notations}



\subsection{A class for ordinal notations}
\subsection{Classes for ordinal notations}

From the \coq{} user's point of view, an ordinal notation is
a structure allowing to compare two ordinals by computation, and proving by well-founded induction.

\subsubsection{The \texttt{Comparable class}}
\subsubsection{The \texttt{Comparison} and \texttt{Comparable} classes}

The following class, contributed by Jérémy Damour and Théo Zimmermann, allows us to apply generic lemmas and tactics
about decidable strict orders.
We use the operational class \texttt{Comparison} of comparison functions to define the \texttt{Comparable} class, contributed by Jérémy Damour and Théo Zimmermann, which allows us to apply generic lemmas and tactics about decidable strict orders.
The correctness of the comparison function is expressed through Stdlib's type
\texttt{Datatypes.CompareSpec}.

\texttt{Datatypes.CompareSpec} as specialized by \texttt{Datatypes.CompSpec}.

\begin{Coqsrc}
Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
| CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
| CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.

Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
CompareSpec (eq x y) (lt x y) (lt y x).
\end{Coqsrc}

\emph{From Module~\href{../theories/html/hydras.Prelude/mparable.html\#Hvariant}{Prelude.Comparable}}
Expand Down
60 changes: 32 additions & 28 deletions theories/gaia/T1Bridge.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,7 @@
(** * Bridge between Hydra-battle's and Gaia's [T1] (Experimental)
*)




From hydras Require Import DecPreOrder.
From hydras Require T1.
From mathcomp Require Import all_ssreflect zify.
From gaia Require Import ssete9.
Expand Down Expand Up @@ -109,18 +107,18 @@ Proof.
Qed.

Lemma compare_ref x :
forall y, match T1.compare x y with
forall y, match T1.compare_T1 x y with
| Lt => T1lt (iota x) (iota y)
| Eq => iota x = iota y
| Gt => T1lt (iota y) (iota x)
end.
Proof.
elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2.
case H: (T1.compare x1 y1).
case H: (T1.compare_T1 x1 y1).
- specialize (IHx1 y1); rewrite H in IHx1.
case H0: (PeanoNat.Nat.compare n n0).
+ have ->: (n = n0) by apply Compare_dec.nat_compare_eq.
case H1: (T1.compare x2 y2).
case H1: (T1.compare_T1 x2 y2).
* rewrite IHx1; f_equal.
by specialize (IHx2 y2); now rewrite H1 in IHx2.
* case (iota x1 < iota y1); [trivial|].
Expand All @@ -141,9 +139,10 @@ Qed.
Lemma lt_ref (a b : hT1): T1.lt a b <-> (iota a < iota b).
Proof.
split.
- rewrite /T1.lt; move => Hab; generalize (compare_ref a b); now rewrite Hab.
- rewrite /T1.lt /Comparable.compare; move => Hab.
generalize (compare_ref a b); now rewrite Hab.
- move => Hab; red.
case_eq (T1.compare a b).
case_eq (T1.compare_T1 a b).
+ move => Heq; generalize (compare_ref a b); rewrite Heq.
move => H0; move: Hab; rewrite H0;
move => Hb; by rewrite T1ltnn in Hb.
Expand All @@ -166,11 +165,12 @@ Qed.
Lemma plus_ref : refines2 T1.plus T1add.
Proof.
move => x; elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2.
case Hx1y1: (T1.compare x1 y1); move: (compare_ref x1 y1); rewrite Hx1y1 => H.
- by rewrite H T1ltnn /=; f_equal.
- by rewrite H /=; f_equal.
case Hx1y1: (T1.compare_T1 x1 y1); move: (compare_ref x1 y1); rewrite Hx1y1 => H.
- rewrite /Comparable.compare H T1ltnn /=; f_equal.
by rewrite Hx1y1 -H /=.
- by rewrite /Comparable.compare H Hx1y1.
- replace (iota x1 < iota y1) with false.
rewrite H /=; f_equal.
rewrite /Comparable.compare H /= Hx1y1; f_equal.
change (cons (iota y1) n0 (iota y2)) with (iota (T1.ocons y1 n0 y2)).
by rewrite IHx2.
by apply T1lt_anti in H.
Expand Down Expand Up @@ -284,28 +284,32 @@ Proof.
by rewrite -(pi_iota a) -(pi_iota b) -(pi_iota c) !mult_refR mulA.
Qed.


Lemma Comparable_T1lt_eq a b:
Comparable.lt_b a b = (iota a < iota b).
Lemma Comparable_T1lt_eq a b:
bool_decide (T1.lt a b) = (iota a < iota b).
Proof.
rewrite /Comparable.lt_b; generalize (compare_ref a b).
case_eq (T1.compare a b).
- move => _ ->; by rewrite T1ltnn.
- by [].
- move => _ H; case_eq (iota a < iota b).
+ move => H0; have H1 : (iota b < iota b) by
apply T1lt_trans with (iota a).
by rewrite T1ltnn in H1.
+ by [].
rewrite /T1.lt; generalize (compare_ref a b);
rewrite /Comparable.compare /=.
destruct (decide (T1.compare_T1 a b = Lt)).
- have bd := e.
apply (bool_decide_eq_true _) in bd.
by rewrite bd e.
- have bd := n.
apply (bool_decide_eq_false _) in bd.
rewrite bd.
destruct (T1.compare_T1 a b).
* by move => ->; rewrite T1ltnn.
* by [].
* move => Hlt.
symmetry.
apply/negP => Hlt'.
have H1 : (iota b < iota b) by apply T1lt_trans with (iota a).
by rewrite T1ltnn in H1.
Qed.


Lemma nf_ref a : T1.nf_b a = T1nf (iota a).
Proof.
elim: a => //.
- move => a IHa n b IHb; rewrite T1.nf_b_cons_eq; simpl T1nf.
rewrite IHa IHb; change (phi0 (iota a)) with (iota (T1.phi0 a)).
rewrite andbA; cbn; by rewrite Comparable_T1lt_eq.
by rewrite andbA Comparable_T1lt_eq.
Qed.


7 changes: 4 additions & 3 deletions theories/ordinals/Epsilon0/Canon.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Pierre Casteran,
From Coq Require Export Arith Lia.
Import Relations Relation_Operators.

From hydras.Prelude Require Import DecPreOrder.
From hydras.Epsilon0 Require Export T1 E0.

Set Implicit Arguments.
Expand Down Expand Up @@ -916,20 +917,20 @@ Fixpoint approx alpha beta fuel i :=
FO => None
| Fuel.FS f =>
let gamma := canonS alpha i in
if lt_b beta gamma
if decide (lt beta gamma)
then Some (i,gamma)
else approx alpha beta (f tt) (S i)
end.


Lemma approx_ok alpha beta :
forall fuel i j gamma, approx alpha beta fuel i = Some (j,gamma) ->
gamma = canonS alpha j /\ lt_b beta gamma.
gamma = canonS alpha j /\ lt beta gamma.
Proof.
induction fuel as [| f IHfuel ].
- cbn; discriminate.
- intros i j gamma H0; cbn in H0.
case_eq (lt_b beta (canonS alpha i));intro H1; rewrite H1 in *.
destruct (decide (lt beta (canonS alpha i))) as [H1|H1].
+ injection H0; intros; subst; split;auto.
+ now specialize (IHfuel tt (S i) _ _ H0).
Qed.
Expand Down
9 changes: 4 additions & 5 deletions theories/ordinals/Epsilon0/E0.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -316,12 +316,11 @@ Proof.
apply LT_trans.
Qed.

Definition compare (alpha beta:E0): comparison :=
T1.compare (cnf alpha) (cnf beta).
Instance compare_E0 : Compare E0 :=
fun (alpha beta:E0) => compare (cnf alpha) (cnf beta).

Lemma compare_correct alpha beta :
CompareSpec (alpha = beta) (alpha o< beta) (beta o< alpha)
(compare alpha beta).
Lemma compare_correct (alpha beta : E0) :
CompSpec eq Lt alpha beta (compare alpha beta).
Proof.
destruct alpha, beta; unfold compare, Lt; cbn;
destruct (T1.compare_correct cnf0 cnf1).
Expand Down
11 changes: 6 additions & 5 deletions theories/ordinals/Epsilon0/Hessenberg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -359,8 +359,9 @@ Proof.
- intros; rewrite (oplus_eqn (ocons a n b) (ocons x1 n0 x2)).
apply nf_helper_phi0 in H1.
destruct (lt_inv H1).
+ unfold T1.lt, lt_b in H2; rewrite compare_rev.
destruct (compare x1 a);auto; try discriminate.
+ unfold T1.lt in H2.
rewrite compare_rev, H2.
reflexivity.
+ decompose [or and] H2.
* inversion H5.
* T1_inversion H6.
Expand Down Expand Up @@ -522,7 +523,7 @@ Section Proof_of_oplus_lt1.
- simpl; auto with T1.
- rewrite oplus_eqn;case_eq (compare x1 a1).
+ auto with T1 arith.
+ intros H2; apply head_lt; unfold T1.lt, lt_b; now rewrite H2.
+ intros H2; apply head_lt. unfold T1.lt; now rewrite H2.
+ intro; apply tail_lt, H1 ; trivial.
eapply nf_inv2, H.
now apply tail_lt_ocons.
Expand Down Expand Up @@ -619,7 +620,7 @@ Proof with eauto with T1.
absurd (T1.lt (ocons a1 n0 b2) (ocons c1 n1 c2)).
- apply lt_not_gt.
apply head_lt.
unfold T1.lt, lt_b;rewrite compare_rev. now rewrite H2.
unfold T1.lt;rewrite compare_rev. now rewrite H2.
- auto.
}
{
Expand Down Expand Up @@ -652,7 +653,7 @@ Proof with eauto with T1.
case_eq (compare a1 c2_1).
intro.
apply coeff_lt; auto with arith.
intro H6; apply head_lt; unfold T1.lt, lt_b; now rewrite H6.
intro H6; apply head_lt; unfold T1.lt; now rewrite H6.
intros; apply tail_lt.
apply oplus_lt1; trivial.
T1_inversion H5.
Expand Down
55 changes: 33 additions & 22 deletions theories/ordinals/Epsilon0/Paths.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@

(** TODO: Check wether the predicates ...PathS... are still useful *)

Require Import Canon MoreLists First_toggle OrdNotations.
From hydras Require Import DecPreOrder Canon MoreLists First_toggle OrdNotations.
Import Relations Relation_Operators.
From Coq Require Import Lia.

Expand Down Expand Up @@ -2592,23 +2592,22 @@ Section Constant_to_standard_Proof.
unfold t; pattern (proj1_sig Rem2); apply proj2_sig.
Qed.

Let P (i:nat) := le_b beta (standard_gnaw (S n) alpha i).
Let P (i:nat) := compare (standard_gnaw (S n) alpha i) beta <> Datatypes.Lt.

Remark Rem04 : P 0.
Proof.
unfold P;red; simpl.
unfold le_b, lt_b.
eenough (T1.compare alpha beta = Datatypes.Gt) as -> by auto.
unfold P;red; simpl.
enough (Hgt: (compare alpha beta = Datatypes.Gt)) by congruence.
apply compare_gt_iff.
generalize (const_pathS_LT Halpha Hpa).
destruct 1; tauto.
Qed.
Qed.


Remark Rem05 : P t = false.
Remark Rem05 : ~ P t.
Proof.
unfold P, le_b, lt_b;
enough(T1.compare (standard_gnaw (S n) alpha t) beta = Datatypes.Lt) as -> by reflexivity.
unfold P.
enough (compare (standard_gnaw (S n) alpha t) beta = Datatypes.Lt) by congruence.
apply compare_lt_iff.
destruct Rem03; tauto.
Qed.
Expand All @@ -2621,8 +2620,21 @@ Section Constant_to_standard_Proof.
eapply const_pathS_LT; eauto.
- auto with arith.
Qed.

Instance P_dec i : Decision (P i).
Proof.
destruct (compare (standard_gnaw (S n) alpha i) beta) eqn:Hc.
- left; unfold P.
rewrite Hc; discriminate.
- right; unfold P.
rewrite Hc.
intro H.
contradiction.
- left; unfold P.
rewrite Hc; discriminate.
Defined.

Let l_def := first_toggle P 0 t Rem06 Rem04 Rem05.
Let l_def := first_toggle P P_dec 0 t Rem06 Rem04 Rem05.

Let l := proj1_sig l_def.

Expand All @@ -2633,21 +2645,21 @@ Section Constant_to_standard_Proof.
(l < t)%nat /\
(forall i : nat,
(0 <= i)%nat ->
(i <= l)%nat -> P i = true) /\ P (S l) = false.
(i <= l)%nat -> P i) /\ ~ P (S l).
Proof.
unfold l; pattern (proj1_sig l_def); apply proj2_sig.
Qed.

Remark Rem09 : (l < t)%nat.
Proof. destruct Rem08; tauto. Qed.

Remark Rem10 : P l = true.
Remark Rem10 : P l.
Proof.
destruct Rem08 as [H H0];decompose [and] H0.
apply H3; auto with arith.
Qed.

Remark Rem11 : P (S l) = false.
Remark Rem11 : ~ P (S l).
Proof.
destruct Rem08 as [H H0]; now decompose [and] H0.
Qed.
Expand Down Expand Up @@ -2726,13 +2738,13 @@ Section Constant_to_standard_Proof.

Remark R19 : beta t1<= gamma.
Proof.
generalize Rem10; unfold P; fold gamma ;unfold le_b, lt_b.
generalize Rem10; unfold P; fold gamma.
intro H.
destruct (T1.compare gamma beta) eqn: Hcomp.
destruct (compare gamma beta) eqn: Hcomp.
- apply compare_eq_iff in Hcomp as ->.
apply LE_refl.
eapply LT_nf_r; eauto.
- intros; discriminate.
- contradiction.
- apply LE_r.
rewrite compare_gt_iff in Hcomp; repeat split; auto.
+ eapply LT_nf_r; eauto.
Expand Down Expand Up @@ -2787,15 +2799,14 @@ Section Constant_to_standard_Proof.

Remark R25 : delta t1< beta.
Proof.
rewrite R22; generalize Rem11;unfold P; intro H;
unfold le_b, lt_b in H.
destruct( T1.compare (standard_gnaw (S n) alpha (S l)) beta) eqn: H0.
- discriminate.
rewrite R22; generalize Rem11;unfold P; intro H.
destruct(compare (standard_gnaw (S n) alpha (S l)) beta) eqn: H0.
- contradict H; congruence.
- rewrite compare_lt_iff in H0.
repeat split;auto.
+ apply standard_gnaw_nf;auto.
+ eapply LT_nf_r; eauto.
- discriminate.
- contradict H; congruence.
Qed.

Remark R26 : ~ const_pathS (n+l) gamma beta.
Expand Down Expand Up @@ -3021,7 +3032,7 @@ Proof.
red in H0;unfold E0.cnf; simpl in *.
destruct beta.
+ destruct H; now apply E0_eq_intro.
+ destruct (T1.compare alpha beta1) eqn:H2.
+ destruct (compare alpha beta1) eqn:H2.
* unfold lt in H1; simpl in H1.
rewrite compare_eq_iff in H2; subst beta1.
destruct (LT_inv H1).
Expand Down
Loading