Stdpp compat

theories/gaia/T1Bridge.v

@@ -1,6 +1,7 @@
 (**  * Bridge between Hydra-battle's and Gaia's [T1]  (Experimental) 
  *)
 
+From hydras Require Export STDPP_compat.
 From hydras Require Import DecPreOrder.
 From hydras Require T1 E0.
 From mathcomp Require Import all_ssreflect zify.

theories/ordinals/Epsilon0/Canon.v

@@ -99,7 +99,7 @@ Proof.
 Qed.
 
 
-Lemma canonS_lim1 : forall i lambda, nf lambda -> limitb lambda 
+Lemma canonS_lim1 : forall i lambda, nf lambda -> limitP lambda 
                                  -> canon (ocons lambda 0 zero) (S i) =
                                     T1.phi0 (canon lambda (S i)).
 Proof.
@@ -110,7 +110,7 @@ Proof.
      + rewrite pred_of_limit;auto.
 Qed.
 
-Lemma canon_lim1 : forall i lambda, nf lambda -> limitb lambda 
+Lemma canon_lim1 : forall i lambda, nf lambda -> limitP lambda 
                                     -> canon (ocons lambda 0 zero)  i =
                                        T1.phi0 (canon lambda i).
 Proof.
@@ -126,7 +126,7 @@ Qed.
 (** Here *)
 
 Lemma canonS_lim2  i n lambda: 
-    nf lambda -> limitb lambda 
+    nf lambda -> limitP lambda 
     -> canon (ocons lambda (S n) zero) (S i) =
        ocons  lambda n (T1.phi0 (canon lambda (S i))).
 Proof.
@@ -139,7 +139,7 @@ Proof.
 Qed.
 
 Lemma canon0_lim2   n lambda: 
-    nf lambda -> limitb lambda 
+    nf lambda -> limitP lambda 
     -> canon (ocons lambda (S n) zero) 0 =
        ocons  lambda n (T1.phi0 (canon lambda 0)).
 Proof.
@@ -150,7 +150,7 @@ Proof.
 Qed.
 
 Lemma canon_lim2  i  n lambda : 
-    nf lambda -> limitb lambda 
+    nf lambda -> limitP lambda 
     -> canon (ocons lambda (S n) zero) i =
        ocons  lambda n (T1.phi0 (canon lambda i)).
 Proof.
@@ -566,7 +566,7 @@ Qed.
 
 
 Lemma limitb_canonS_not_zero i lambda:
-  nf lambda -> limitb lambda  -> canon lambda (S i) <> zero.
+  nf lambda -> limitP lambda  -> canon lambda (S i) <> zero.
 Proof.
   destruct lambda as [ | alpha1 n alpha2].
   - discriminate.
@@ -599,7 +599,7 @@ limit of its  own canonical sequence
 (*| .. coq:: no-out *)
 Lemma canonS_limit_strong lambda : 
   nf lambda ->
-  limitb lambda  ->
+  limitP lambda  ->
   forall beta, beta t1< lambda ->
                {i:nat | beta t1< canon lambda (S i)}.
 Proof.
@@ -775,7 +775,7 @@ Defined.
 
 Lemma canon_limit_strong lambda : 
   nf lambda ->
-  limitb lambda  ->
+  limitP lambda  ->
   forall beta, beta t1< lambda ->
                 {i:nat | beta t1< canon lambda i}.
 Proof.
@@ -786,7 +786,7 @@ Defined.
 (* begin snippet canonSLimitLub *)
 
 Lemma canonS_limit_lub (lambda : T1) :
-  nf lambda -> limitb lambda  ->
+  nf lambda -> limitP lambda  ->
   strict_lub (canonS lambda) lambda. (* .no-out *) (*| .. coq:: none |*)
 Proof.
   split.
@@ -813,7 +813,7 @@ Qed.
 (* end snippet canonSLimitLub *)
 
 
-Lemma canonS_limit_mono alpha i j : nf alpha -> limitb alpha  ->
+Lemma canonS_limit_mono alpha i j : nf alpha -> limitP alpha  ->
                                     i < j ->
                                     canonS alpha i t1< canonS alpha j.
 Proof. 
@@ -992,7 +992,7 @@ Proof.
       apply LT1; apply nf_phi0;auto with E0.
 Qed. 
 
-Lemma CanonS_phi0_lim alpha k : Limitb alpha ->
+Lemma CanonS_phi0_lim alpha k : LimitP alpha ->
                                 CanonS (phi0 alpha) k =
                                 phi0 (CanonS alpha k). 
 Proof.
@@ -1023,7 +1023,7 @@ Proof.
   -   apply CanonS_lt.
 Qed.
 
-Lemma Canon_of_limit_not_null : forall i alpha, Limitb alpha ->
+Lemma Canon_of_limit_not_null : forall i alpha, LimitP alpha ->
                                        Canon alpha (S i) <> Zero.
 Proof.
   destruct alpha;simpl;unfold CanonS; simpl;  rewrite E0_eq_iff.

theories/ordinals/Epsilon0/E0.v

@@ -74,6 +74,9 @@ Definition Limitb (alpha : E0) : bool :=
 Definition Succb (alpha : E0) : bool :=
   succb (@cnf alpha).
 
+Notation LimitP alpha := (is_true (Limitb alpha)).
+Notation SuccP alpha := (is_true (Succb alpha)).
+
 
 #[global] Instance ord1 : E0.
 Proof. 
@@ -214,7 +217,7 @@ Qed.
 
 
 
-Lemma Succb_Succ alpha : Succb alpha -> {beta : E0 | alpha = Succ beta}.
+Lemma Succb_Succ alpha : SuccP alpha -> {beta : E0 | alpha = Succ beta}.
 Proof.
   destruct alpha; cbn.
   intro H; destruct (succb_def cnf_ok0 H) as [beta [Hbeta Hbeta']]; subst.
@@ -263,7 +266,7 @@ Lemma cnf_Omega_term (alpha: E0) (n: nat) :
 Proof. reflexivity. Defined.
 
 Lemma Limitb_Omega_term alpha i : alpha <> Zero ->
-                                  Limitb (Omega_term alpha i).
+                                  LimitP (Omega_term alpha i).
 Proof.
   intro H; unfold Limitb; destruct alpha as [cnf0 H0]; cbn;
     destruct cnf0.
@@ -272,7 +275,7 @@ Proof.
 Qed.
 
 Lemma Limitb_phi0 alpha  : alpha <> Zero ->
-                           Limitb (phi0 alpha).
+                           LimitP (phi0 alpha).
 Proof.
   unfold phi0; apply Limitb_Omega_term.
 Qed.
@@ -394,7 +397,7 @@ Qed.
 Global Hint Resolve Pred_Lt : E0.
 
 
-Lemma Succ_Succb (alpha : E0) : Succb (Succ alpha).
+Lemma Succ_Succb (alpha : E0) : SuccP (Succ alpha).
 destruct alpha; unfold Succb, Succ; cbn; apply T1.succ_succb.
 Qed.
 
@@ -420,14 +423,14 @@ Qed.
 
 Hint Rewrite FinS_Succ_eq : E0_rw.
 
-Lemma Limit_not_Zero alpha : Limitb alpha -> alpha <> Zero.
+Lemma Limit_not_Zero alpha : LimitP alpha -> alpha <> Zero.
 Proof.
   destruct alpha; unfold Limitb, Zero; cbn; intros H H0.
   injection H0;  intro ; subst cnf0; eapply T1.limitb_not_zero; eauto.
 Qed.
 
 
-Lemma Succ_not_Zero alpha:  Succb alpha -> alpha <> Zero.
+Lemma Succ_not_Zero alpha:  SuccP alpha -> alpha <> Zero.
 Proof.
   destruct alpha;unfold Succb, Zero; cbn.
   intros H H0; injection H0; intro;subst; discriminate H.
@@ -439,7 +442,7 @@ Proof.
 Qed.
 
 
-Lemma Succ_not_Limitb alpha : Succb alpha -> ~ Limitb alpha .
+Lemma Succ_not_Limitb alpha : SuccP alpha -> ~ LimitP alpha .
 Proof. 
   red; destruct alpha; unfold Succb, Limitb; cbn.
   intros H H0. rewrite (succ_not_limit _ H) in H0. discriminate.  
@@ -465,7 +468,7 @@ Proof.
 Qed.
 
 Lemma Succ_lt_Limitb alpha beta:
-    Limitb alpha ->  beta o< alpha -> Succ beta o< alpha.
+    LimitP alpha ->  beta o< alpha -> Succ beta o< alpha.
 Proof.
   destruct alpha, beta;unfold Lt; cbn.
   intros; apply succ_lt_limit; auto. 
@@ -615,8 +618,8 @@ Proof.
 Defined.
 
 Lemma Limitb_plus alpha beta i:
-  (beta o< phi0 alpha)%e0 -> Limitb beta ->
-  Limitb (Omega_term alpha i + beta)%e0.
+  (beta o< phi0 alpha)%e0 -> LimitP beta ->
+  LimitP (Omega_term alpha i + beta)%e0.
 Proof.
   intros H H0;  assert (alpha <> Zero).
   { intro; subst. 
@@ -798,7 +801,7 @@ Proof.
   - right; now apply Lt_Le_incl.
 Qed.
 
-Lemma Limit_gt_Zero (alpha: E0) : Limitb alpha -> Zero o< alpha.
+Lemma Limit_gt_Zero (alpha: E0) : LimitP alpha -> Zero o< alpha.
 Proof.
   intro H; destruct (E0_lt_eq_lt alpha Zero) as [H0 | [H0 | H0]]; trivial.
   - destruct (E0_not_Lt_zero H0).

theories/ordinals/Epsilon0/F_alpha.v

@@ -115,7 +115,7 @@ Proof.
 Qed.
 
 Lemma F_eq2 : forall alpha i,
-    Succb alpha -> 
+    SuccP alpha -> 
     F_ alpha i = F_star (Pred alpha, S i) i.
 Proof.
   unfold F_; intros; rewrite F_star_equation_2.
@@ -161,7 +161,7 @@ Qed.
 (*||*)
 
 Lemma F_lim_eqn : forall alpha i,
-    Limitb alpha ->
+    LimitP alpha ->
     F_ alpha i = F_ (Canon alpha i) i. (* .no-out *)
 (*| .. coq:: none |*)
 Proof.
@@ -415,7 +415,7 @@ Section Properties.
 
 
     Section alpha_limit.
-      Hypothesis Hlim : Limitb alpha.
+      Hypothesis Hlim : LimitP alpha.
 
 
       Remark RBlim : forall n, n < F_ alpha n.
@@ -735,7 +735,7 @@ Let P (alpha: E0) := forall n,  (F_ alpha (S n) <= H'_ (phi0 alpha) (S n))%nat.
    - now apply E0_eq_intro.
  Qed.
 
- Lemma HFsucc : Succb alpha -> P alpha.
+ Lemma HFsucc : SuccP alpha -> P alpha.
  Proof.
    intro H; destruct (Succb_Succ _ H) as [beta Hbeta]; subst.
    intro n; rewrite H'_Phi0_succ.
@@ -754,7 +754,7 @@ Let P (alpha: E0) := forall n,  (F_ alpha (S n) <= H'_ (phi0 alpha) (S n))%nat.
   (** The following proof is far from being trivial.
       It uses some lemmas from the Ketonen-Solovay machinery *)
 
-  Lemma HFLim : Limitb alpha -> P alpha.
+  Lemma HFLim : LimitP alpha -> P alpha.
   Proof.
     intros Halpha n; rewrite H'_eq3.
     - rewrite CanonS_Canon;
@@ -863,7 +863,7 @@ Proof.
 Qed.
 
 Lemma f_eq2 : forall alpha i,
-    Succb alpha -> 
+    SuccP alpha -> 
     f_ alpha i = f_star (Pred alpha,  i) i.
 Proof.
   unfold f_; intros; rewrite f_star_equation_2.
@@ -906,7 +906,7 @@ Proof.
 Qed.
 
 
-Lemma f_lim_eqn : forall alpha i,  Limitb alpha ->
+Lemma f_lim_eqn : forall alpha i,  LimitP alpha ->
                                    f_ alpha i = f_ (Canon alpha i) i.
 Proof.
   unfold f_; intros. rewrite f_star_equation_2.

theories/ordinals/Epsilon0/Hprime.v

@@ -57,7 +57,7 @@ Qed.
 
 (* begin snippet paraphrasesb:: no-out  *)
 Lemma H'_eq2 alpha i :
-  Succb alpha ->
+  SuccP alpha ->
   H'_ alpha i = H'_ (Pred alpha) (S i).
 (* end snippet paraphrasesb *)
 
@@ -72,7 +72,7 @@ Qed.
 
 (* begin snippet paraphrasesc:: no-out  *)
 Lemma H'_eq3 alpha i :
-  Limitb alpha ->
+  LimitP alpha ->
   H'_ alpha i =  H'_ (Canon alpha (S i)) i.
 (* end snippet paraphrasesc *)
 
@@ -702,7 +702,7 @@ Section Proof_of_Abstract_Properties.
 
 
     Section alpha_limit.
-      Hypothesis Hlim : Limitb alpha.
+      Hypothesis Hlim : LimitP alpha.
 
       Remark RBlim : forall n, (n < H'_ alpha n)%nat.
       Proof.
@@ -918,7 +918,7 @@ Section Proof_of_H'_mono_l.
   End Succ_case.
 
   Section Limit_case.
-    Hypothesis Hbeta: Limitb beta.
+    Hypothesis Hbeta: LimitP beta.
 
     Remark R4 : Succ alpha o< beta.
     Proof. now apply Succ_lt_Limitb. Qed.

theories/ordinals/Epsilon0/L_alpha.v

@@ -46,7 +46,7 @@ Lemma L_zero_eqn : forall i, L_ Zero i = i.
 Proof. intro i; now rewrite L__equation_1. Qed.
 
 Lemma L_eq2 alpha i :
-  Succb alpha -> L_ alpha i = L_ (Pred alpha) (S i).
+  SuccP alpha -> L_ alpha i = L_ (Pred alpha) (S i).
 (* end snippet Paraphrasesa *)
 
 Proof.
@@ -72,7 +72,7 @@ Hint Rewrite L_zero_eqn L_succ_eqn : L_rw.
 
 (* begin snippet Paraphrasesc:: no-out *)
 Lemma L_lim_eqn alpha i :
-  Limitb alpha ->
+  LimitP alpha ->
   L_ alpha i = L_ (Canon alpha i) (S i).
 (* end snippet Paraphrasesc *)
 
@@ -195,12 +195,12 @@ Section L_correct_proof.
 
   Lemma L_ok_lim  alpha  :
     (forall beta,  (beta o< alpha)%e0 -> P beta) ->
-    Limitb alpha -> P alpha.
+    LimitP alpha -> P alpha.
   Proof with eauto with E0.
     unfold P; intros.
     apply L_spec_compat with (fun k =>  L_ (Canon alpha k) (S k)).
     -   generalize L_lim_ok; intro H1; unfold L_lim in H1.
-       assert (H2 : limitb (cnf alpha)) by (now destruct alpha). 
+       assert (H2 : limitP (cnf alpha)) by (now destruct alpha). 
        specialize (H1 (cnf alpha) cnf_ok H2 (fun k i => L_ (Canon alpha k) i)).
        apply H1; intro k; specialize (H (Canon alpha  (S k))).
        assert  (H3: (Canon alpha (S k) o< alpha)%e0 ).

theories/ordinals/Epsilon0/Large_Sets.v

@@ -329,7 +329,7 @@ End succ.
 Section lim.
   Variables (lambda : T1)
             (Hnf : nf lambda)
-            (Hlim : limitb lambda)
+            (Hlim : limitP lambda)
             (f : nat -> nat -> nat)
             (H : forall k, L_spec (canon lambda (S k)) (f (S k))).
 
@@ -817,7 +817,7 @@ Definition largeb (alpha : T1) (s: list nat) :=
           with zero => true | _ => false end.
 
 Definition large (alpha : T1) (s : list nat) : Prop :=
-  largeb alpha s.
+  is_true (largeb alpha s).
 
 (* end snippet largeDef *)
 
@@ -829,7 +829,7 @@ Definition largeSb (alpha : T1) (s: list nat) :=
   end.
 
 Definition largeS (alpha : T1) (s : list nat) : Prop :=
-  largeSb alpha s.
+  is_true (largeSb alpha s).
 
 
 Definition Large alpha s := large (@cnf alpha) s.