Add a coercion from ON to Wf

coq-community · Jan 23, 2024 · 14bf0de · 14bf0de
1 parent 51bf7cf
commit 14bf0de
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 12 deletions.
diff --git a/theories/ordinals/Hydra/Hydra_Termination.v b/theories/ordinals/Hydra/Hydra_Termination.v
@@ -7,6 +7,7 @@ Set Program Cases.
 
 From hydras Require Export Hydra_Lemmas.
 From hydras Require Import E0 Hessenberg.
+Import ON_Generic. 
 
 (** ***  Converting any hydra into an ordinal less than 
   #epsilon0# $\epsilon_0$  
@@ -194,8 +195,7 @@ Qed.
 #[ global, program ] Instance var (h:Hydra) : E0:= @mkord (m h) _.
 Next Obligation. apply m_nf. Defined.
 
-
-#[global] Instance HVariant_0 : @Hvariant _ _ T1_wf free m.
+#[global] Instance HVariant_0 : Hvariant T1_wf free m.
 Proof.
  split; intros; eapply round_decr; eauto.
 Qed.
@@ -204,8 +204,7 @@ Qed.
 (* begin snippet FinalThm *)
 
 (*| .. coq:: no-out |*)
-
-#[global] Instance HVariant : Hvariant E0lt_wf free var.
+#[global] Instance HVariant : Hvariant Epsilon0 free var.
 Proof.
  split; intros; eapply round_decr; eauto.
 Qed.

diff --git a/theories/ordinals/Hydra/Omega2_Small.v b/theories/ordinals/Hydra/Omega2_Small.v
@@ -21,7 +21,7 @@ Section Impossibility_Proof.
 
   Variable m : Hydra -> ON_Omega2.t.
   Context
-    (Hvar: Hvariant (ON_Generic.ON_wf (ON:=Omega2)) free m).
+    (Hvar: Hvariant Omega2 free m).
 
   (* end snippet Impossibilitya *)
 

diff --git a/theories/ordinals/Hydra/Omega_Small.v b/theories/ordinals/Hydra/Omega_Small.v
@@ -3,12 +3,10 @@
 
 
 From Coq Require Import   Arith Lia.
-From hydras Require Import Hydra_Lemmas.
+From hydras Require Import Hydra_Lemmas ON_Generic ON_Omega.
 Open Scope nat_scope.
 
-
-
-#[ global ] Instance height_var : @Hvariant  _ _ lt_wf free height.
+#[global] Instance height_var : Hvariant Omega free height.
 Proof.
   split;intros.
 (*
@@ -28,7 +26,7 @@ Proof.
 Abort.
 (* end show *)
 
-Lemma height_bad :  ~ @Hvariant _ _ lt_wf free height.
+Lemma height_bad :  ~ Hvariant Omega free height.
 Proof.
   intros [H];
   specialize (H 1 (hyd1 (hyd2 head head))  (hyd1 (hyd1 head)));
@@ -51,7 +49,7 @@ Section Impossibility_Proof.
       for proving the termination of all hydra battles *)
 
   Variable m : Hydra -> nat.
-  Context (Hvar : @Hvariant _ _ lt_wf free m).
+  Context (Hvar : Hvariant lt_wf free m).
 
 (* end snippet omegaSmalla *)
 

diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -24,9 +24,11 @@ Delimit Scope ON_scope with on.
 Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
   {
   ON_comp :> Comparable lt cmp;
-  ON_wf : well_founded lt;
+  ON_wf :> well_founded lt;
   }.
 #[global] Existing Instance ON_comp.
+Coercion ON_wf :  ON >-> well_founded.
+
 (* end snippet ONDef *)
 
 (* begin snippet ONDefsa:: no-out  *)