text:
(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(*****************************************************************************)
(*          Projet Formel - Calculus of Inductive Constructions V5.10        *)
(*****************************************************************************)
(*									     *)
(*	       Category Parallel Arrowd (used in Equalizers)		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export BasicTypes.
Require Export Category.

Set Implicit Arguments.
Unset Strict Implicit.

Section pa_def.

Variables (C : Category) (a b : C) (I : Type) (k : I -> (a --> b)).

Inductive PA_ob : Type :=
  | PA1 : PA_ob
  | PA2 : PA_ob.

Inductive PA_mor : PA_ob -> PA_ob -> Type :=
  | PA_I1 : PA_mor PA1 PA1
  | PA_I2 : PA_mor PA2 PA2
  | PA_f : I -> PA_mor PA1 PA2.

(* sche'mas d'e'limination pour PA_mor *)

Lemma PA_11_P :
 (PA_mor PA1 PA1 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
intros P x y; elim x; elim y.
exact P.
intro x'; exact True.
intro x'; exact True.
intro x'; exact True.
Defined.

Lemma PA_11_ind :
 forall P : PA_mor PA1 PA1 -> Prop, P PA_I1 -> forall x : PA_mor PA1 PA1, P x.
Proof.
intros P PP1 x.
change (PA_11_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_11_P P f));
 simpl in |- *.
exact PP1.
trivial.
trivial.
Qed.

Lemma PA_22_P :
 (PA_mor PA2 PA2 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
intros P x y; elim x; elim y.
intro x'; exact True.
intro x'; exact True.
intro x'; exact True.
exact P.
Defined.

Lemma PA_22_ind :
 forall P : PA_mor PA2 PA2 -> Prop, P PA_I2 -> forall x : PA_mor PA2 PA2, P x.
Proof.
intros P PP2 x.
change (PA_22_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_22_P P f));
 simpl in |- *.
trivial.
exact PP2.
trivial.
Qed.

Lemma PA_12_P :
 (PA_mor PA1 PA2 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
intros P x y; elim x; elim y.
intro x'; exact True.
exact P.
intro x'; exact True.
intro x'; exact True.
Defined.

Lemma PA_12_ind :
 forall P : PA_mor PA1 PA2 -> Prop,
 (forall i : I, P (PA_f i)) -> forall x : PA_mor PA1 PA2, P x.
Proof.
intros P Pf x.
change (PA_12_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_12_P P f));
 simpl in |- *.
trivial.
trivial.
exact Pf.
Qed.

Lemma PA_21_P :
 (PA_mor PA2 PA1 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
intros P x y; elim x; elim y.
intro x'; exact True.
intro x'; exact True.
exact P.
intro x'; exact True.
Defined.

Lemma PA_21_ind :
 forall (P : PA_mor PA2 PA1 -> Prop) (x : PA_mor PA2 PA1), P x.
Proof.
intros P x.
change (PA_21_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_21_P P f));
 simpl in |- *; auto.
Qed.

Lemma PA_21_T :
 (PA_mor PA2 PA1 -> Type) -> forall x y : PA_ob, PA_mor x y -> Type.
Proof.
intros P x y; elim x; elim y.
intro x'; exact UnitType.
intro x'; exact UnitType.
exact P.
intro x'; exact UnitType.
Defined.

Lemma PA_21_rect :
 forall (P : PA_mor PA2 PA1 -> Type) (x : PA_mor PA2 PA1), P x.
Proof.
intros P x.
change (PA_21_T P x) in |- *.
apply (PA_mor_rect (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_21_T P f));
 simpl in |- *; auto.
Qed.

(* egalite' *)

Definition Equal_PA_mor (x y : PA_ob) (f g : PA_mor x y) :=
  match f in (PA_mor x' y') return Prop with
  | PA_I1 =>
      (* PA_I1  *)  True
      (* PA_I2  *)
  | PA_I2 => True
      (* PA_f i *)
  | PA_f i =>
      match g in (PA_mor x' y') return Prop with
      | PA_I1 =>
          (* PA_I1  *)  False
          (* PA_I2  *)
      | PA_I2 => False
          (* PA_f j *)
      | PA_f j => k i =_S k j
      end
  end.

Lemma Equal_PA_mor_Equiv :
 forall x y : PA_ob, Equivalence (Equal_PA_mor (x:=x) (y:=y)).
Proof.
intros x y; apply Build_Equivalence;
 [ red in |- * | apply Build_Partial_equivalence; red in |- * ].
intro f; elim f.
simpl in |- *; trivial.
simpl in |- *; trivial.
intro i; simpl in |- *; apply Refl.
intros f; elim f.
intros g h e1 e2.
apply (PA_11_ind (P:=fun h : PA_mor PA1 PA1 => Equal_PA_mor PA_I1 h)).
simpl in |- *; trivial.
intros g h e1 e2.
apply (PA_22_ind (P:=fun h : PA_mor PA2 PA2 => Equal_PA_mor PA_I2 h)).
simpl in |- *; trivial.
intros i g h.
lapply
 (PA_12_ind
    (P:=fun x : PA_mor PA1 PA2 =>
        Equal_PA_mor (PA_f i) x ->
        Equal_PA_mor x h -> Equal_PA_mor (PA_f i) h)).
intros H H0 H1; apply (H g H0 H1).
intro j; unfold Equal_PA_mor at 1 in |- *; intro eqij.
lapply
 (PA_12_ind
    (P:=fun x : PA_mor PA1 PA2 =>
        Equal_PA_mor (PA_f j) x -> Equal_PA_mor (PA_f i) x)).
intros H H0; apply (H h H0).
simpl in |- *; intros l eqjl.
(* *) apply Trans with (k j); trivial.
intros f; elim f.
intros g e1.
apply (PA_11_ind (P:=fun g : PA_mor PA1 PA1 => Equal_PA_mor g PA_I1)).
simpl in |- *; trivial.
intros g e1.
apply (PA_22_ind (P:=fun g : PA_mor PA2 PA2 => Equal_PA_mor g PA_I2)).
simpl in |- *; trivial.
intros i g.
lapply
 (PA_12_ind
    (P:=fun g : PA_mor PA1 PA2 =>
        Equal_PA_mor (PA_f i) g -> Equal_PA_mor g (PA_f i))).
intros H H0; apply (H g H0).
intro j; simpl in |- *; intro eqij; apply Sym; trivial.
Qed.

Canonical Structure PA_mor_setoid (x y : PA_ob) :=
  Build_Setoid (Equal_PA_mor_Equiv x y).

(* composition *)

Definition Comp_PA_mor (x y z : PA_ob) (f : PA_mor x y) :=
  match f in (PA_mor p p0) return (PA_mor p0 z -> PA_mor p z) with
  | PA_I1 =>
      (* PA_I1 *)
      match z as p return (PA_mor PA1 p -> PA_mor PA1 p) with
      | PA1 =>
          (* PA1 *)  fun _ => PA_I1
                     (* PA2 *)
      | PA2 => fun g => g
      end
      (* PA_I2 *)
  | PA_I2 =>
      match z as p return (PA_mor PA2 p -> PA_mor PA2 p) with
      | PA1 =>
          (* PA1 *)
          fun g => PA_21_rect (fun _ => PA_mor PA2 PA1) g
          (* PA2 *)
      | PA2 => fun _ => PA_I2
      end
      (* PA_f  *)
  | PA_f x =>
      match z as p return (I -> PA_mor PA2 p -> PA_mor PA1 p) with
      | PA1 =>
          (* PA1 *)
          fun _ g => PA_21_rect (fun _ => PA_mor PA1 PA1) g
          (* PA2 *)
      | PA2 => fun i _ => PA_f i
      end x
  end.
(* *)

(* code complique' pour contourner bug Generalize *)

Lemma Comp_PA_fact1 :
 forall (f : PA_mor PA1 PA1) (x : PA_ob) (g : PA_mor PA1 x),
 Comp_PA_mor f g =_S g.
Proof.
intros f x g;
 apply (PA_11_ind (P:=fun x' : PA_mor PA1 PA1 => Comp_PA_mor x' g =_S g)).
generalize g.
elim x.
simpl in |- *; auto.
intro g1; apply Refl.
Qed.

Lemma Comp_PA_fact2 :
 forall (f : PA_mor PA2 PA2) (x : PA_ob) (g : PA_mor PA2 x),
 Comp_PA_mor f g =_S g.
Proof.
intros f x g;
 apply (PA_22_ind (P:=fun x' : PA_mor PA2 PA2 => Comp_PA_mor x' g =_S g)).
generalize g.
elim x.
intro g1;
 apply
  (PA_21_ind
     (fun x' : PA_mor PA2 PA1 =>
      PA_21_rect (fun _ : PA_mor PA2 PA1 => PA_mor PA2 PA1) g1 =_S g1) g1).
simpl in |- *; auto.
Qed.

Lemma Comp_PA_fact3 :
 forall (i : I) (g : PA_mor PA2 PA2), Comp_PA_mor (PA_f i) g =_S PA_f i.
Proof.
intros i g;
 apply
  (PA_22_ind
     (P:=fun x' : PA_mor PA2 PA2 => Comp_PA_mor (PA_f i) x' =_S PA_f i)).
apply Refl.
Qed.

Lemma Comp_PA_fact4 :
 forall (i : I) (g : PA_mor PA2 PA1) (h : PA_mor PA1 PA1),
 Comp_PA_mor (PA_f i) g =_S h.
Proof.
intros i g h;
 apply
  (PA_21_ind (fun x' : PA_mor PA2 PA1 => Comp_PA_mor (PA_f i) g =_S h) g).
Qed.

(** **)

Lemma Comp_PA_congl : Congl_law Comp_PA_mor.
Proof.
unfold Congl_law in |- *.
intros x y z f g h.
generalize f; generalize g.
elim h; elim z.
(* cas 1*)
(* cas 1.1 *)
simpl in |- *; auto.
(* cas 1.2 *)
simpl in |- *; auto.
(* cas 2 *)
(* cas 2.1 *)
intros f0 g0 H.
apply
 (PA_21_ind
    (fun x : PA_mor PA2 PA1 => Comp_PA_mor PA_I2 g0 =_S Comp_PA_mor PA_I2 f0)
    g0).
(* cas 2.2 *)
simpl in |- *; auto.
(* cas 3 *)
(* cas 3.1 *)
intros i g0 f0 H.
apply
 (PA_21_ind
    (fun x : PA_mor PA2 PA1 =>
     Comp_PA_mor (PA_f i) f0 =_S Comp_PA_mor (PA_f i) g0) f0).
(* cas 3.2 *)
intros i g0 f0 H; apply Refl.
Qed.

Lemma Comp_PA_congr : Congr_law Comp_PA_mor.
Proof.
unfold Congr_law in |- *.
intros x y z f; elim f.
(* cas 1 *)
intro g;
 lapply
  (PA_11_ind
     (P:=fun x' : PA_mor PA1 PA1 =>
         forall h : PA_mor PA1 z,
         PA_I1 =_S x' -> Comp_PA_mor PA_I1 h =_S Comp_PA_mor x' h)).
intros H h H0; apply (H g h H0).
elim z.
(* cas 1.1 *)
simpl in |- *; auto.
(* cas 1.2 *)
intros h H; apply Refl.
(* cas 2 *)
intro g;
 lapply
  (PA_22_ind
     (P:=fun x' : PA_mor PA2 PA2 =>
         forall h : PA_mor PA2 z,
         Equal_PA_mor PA_I2 x' -> Comp_PA_mor PA_I2 h =_S Comp_PA_mor x' h)).
intros H h H0; apply (H g h H0).
elim z.
(* cas 2.1 *)
intros h H;
 apply
  (PA_21_ind
     (fun x' : PA_mor PA2 PA1 => Comp_PA_mor PA_I2 h =_S Comp_PA_mor PA_I2 h)
     h).
(* cas 2.2 *)
simpl in |- *; auto.
(* cas 3 *)
intros i g;
 lapply
  (PA_12_ind
     (P:=fun x' : PA_mor PA1 PA2 =>
         forall h : PA_mor PA2 z,
         Equal_PA_mor (PA_f i) x' ->
         Comp_PA_mor (PA_f i) h =_S Comp_PA_mor x' h)).
intros H h H0; apply (H g h H0).
elim z.
(* cas 3.1 *)
intros j h H;
 apply
  (PA_21_ind
     (fun x' : PA_mor PA2 PA1 =>
      Comp_PA_mor (PA_f i) h =_S Comp_PA_mor (PA_f j) h) h).
(* cas 3.2 *)
intros j h H; simpl in |- *; exact H.
Qed.

(** **)

Definition Comp_PA := Build_Comp Comp_PA_congl Comp_PA_congr.

Lemma Assoc_PA : Assoc_law Comp_PA.
Proof.
unfold Assoc_law in |- *.
intros x y z o4 f; elim f.
(* cas 1 *)
intros g h.
apply Trans with (Comp_PA_mor g h).
apply (Comp_PA_fact1 PA_I1 (Comp_PA_mor g h)).
apply (Comp_PA_congr (f:=g) (g:=Comp_PA_mor PA_I1 g) h).
apply Sym.
apply (Comp_PA_fact1 PA_I1 g).
(* cas 2 *)
intros g h.
apply Trans with (Comp_PA_mor g h).
apply (Comp_PA_fact2 PA_I2 (Comp_PA_mor g h)).
apply (Comp_PA_congr (f:=g) (g:=Comp_PA_mor PA_I2 g) h).
apply Sym.
apply (Comp_PA_fact2 PA_I2 g).
(* cas 3 *)
intro i; elim z.
intros g h;
 apply
  (PA_21_ind
     (fun x : PA_mor PA2 PA1 =>
      Comp_PA_mor (PA_f i) (Comp_PA_mor g h) =_S
      Comp_PA_mor (Comp_PA_mor (PA_f i) g) h) g).
intros g h; apply Trans with (Comp_PA_mor (PA_f i) h).
apply (Comp_PA_congl (f:=Comp_PA_mor g h) (g:=h) (PA_f i)).
apply (Comp_PA_fact2 g h).
simpl in |- *.
apply (Comp_PA_congr (f:=PA_f i) (g:=Comp_PA_mor (PA_f i) g) h).
apply Sym.
apply (Comp_PA_fact3 i g).
Qed.

Definition Id_PA (x : PA_ob) :=
  match x as x' return (PA_mor x' x') with
  | PA1 => (* PA1 *)  PA_I1
      (* PA2 *)
  | PA2 => PA_I2
  end.

Lemma Idl_PA : Idl_law Comp_PA Id_PA.
Proof.
unfold Idl_law in |- *; simpl in |- *.
intros x y; elim x; intro f.
apply (Comp_PA_fact1 PA_I1 f).
apply (Comp_PA_fact2 PA_I2 f).
Qed.

Lemma Idr_PA : Idr_law Comp_PA Id_PA.
Proof.
unfold Idr_law in |- *; simpl in |- *.
intros x y f; elim f.
apply (Comp_PA_fact1 PA_I1 PA_I1).
apply (Comp_PA_fact2 PA_I2 PA_I2).
intro i; apply (Comp_PA_fact3 i PA_I2).
Qed.

Canonical Structure PA := Build_Category Assoc_PA Idl_PA Idr_PA.

End pa_def.

author: JasonGross

repo: category-coq-experience-tests


text:
(**************************************************************************)
(*           *                                                            *)
(*     _     *   The Coccinelle Library / Evelyne Contejean               *)
(*    <o>    *          CNRS-LRI-Universite Paris Sud                     *)
(*  -/@|@\-  *                   A3PAT Project                            *)
(*  -@ | @-  *                                                            *)
(*  -\@|@/-  *      This file is distributed under the terms of the       *)
(*    -v-    *      CeCILL-C licence                                      *)
(*           *                                                            *)
(**************************************************************************)

(** * Termination of rewriting *)

From Coq Require Import List Relations Wellfounded Arith Recdef Setoid.
From CoLoR Require Import closure more_list weaved_relation term_spec
     equational_theory_spec.
From CoLoR Require Export dp.

Module MakeIGDP (E : EqTh).

  Import E.
  Import T.
  Module Dp := dp.MakeDP (E).
  Import Dp.

Inductive hide_in_context R : relation term :=
  Hide_in_context : forall f l1 l2, (one_step_list (one_step R)) l1 l2 -> hide_in_context R (Term f l1) (Term f l2).

Lemma expand_dp : forall dpR R t f l,
   rdp_step dpR R t (Term f l) <-> compose_rel dpR (refl_trans_clos (hide_in_context R)) t (Term f l).
Proof.
intros dpR R t f l; split.
intro H; inversion H as [g l1 l2 H1 H2 H3]; subst.
constructor 1 with (Term f l2); trivial.
inversion H2 as [k | k1 k2 K2]; subst.
left.
right; clear -K2; induction K2 as [l1 l2 H | l1 l2 l3 H1 H2].
left; constructor; assumption.
right with (Term f l2); [ constructor | ]; assumption.
intro H; inversion H as [u1 u2 u3 H1 H2]; subst.
assert (K : exists l2, u2 = Term f l2 /\ refl_trans_clos (one_step_list (one_step R)) l2 l).
clear -H2; inversion H2 as [u | u1 v2 K2]; clear H2; subst.
exists l; split; [apply eq_refl | left].
set (s := Term f l) in *.
assert (s_eq_fl := eq_refl s).
unfold s at 2 in s_eq_fl; clearbody s.
revert f l s_eq_fl; induction K2 as [t1 t2 K | t1 t2 t3 K1 K2]; intros f l s_eq_fl.
inversion K as [f' l1 l2]; clear K; subst.
injection H1; clear H1; intros; subst f' l2.
exists l1; split; [apply eq_refl | right; left; assumption].
inversion K1 as [f' l1 l2]; clear K1; subst.
destruct (IHK2 _ _ (eq_refl _)) as [l3 [J1 J2]].
injection J1; clear J1; intros; subst f' l3.
exists l1; split; [apply eq_refl | apply refl_trans_clos_is_trans with l2; [right; left | ]; assumption].
destruct K as [l2 [J1 J2]].
subst u2; constructor 1 with l2; assumption.
Qed.

(* Definition dpi comp i (v u : term) := comp (u,v) = i /\ i <> 0. *)

Lemma split_rel :
  forall dpR R (comp : (term * term) -> nat -> Prop)
  (comp_approx : forall uv uv', are_connected dpR R uv uv' -> forall n n', comp uv n -> comp uv' n' -> n <= n')
  (comp_def_on_dps : forall u v, (exists n, comp (u,v) n) <-> dpR v u)
  (split_graph :
    exists n0,  forall uv n, comp uv n -> n <= n0),
   forall P,  well_founded (rest P (rdp_step (axiom dpR) R))  <->
  (forall n, well_founded (rest P (rdp_step (axiom (fun v u => comp (u,v) n)) R))).
Proof.
intros dpR R comp comp_approx comp_def_on_dps split_graph P.
split; intro W.
intros n; revert W; apply wf_incl; intros s t [K [As At]].
inversion K as [f l1 l2 s' H1 H2]; subst.
inversion H2 as [t1 t2 sigma H3 H4 H5]; subst.
split; [ | split; assumption].
constructor 1 with l2; trivial.
rewrite <- H5; constructor.
rewrite <- comp_def_on_dps; exists n; assumption.

destruct split_graph as [n G].
revert comp comp_approx comp_def_on_dps G W.
induction n as [ | n]; intros  comp comp_approx comp_def_on_dps G W.
(* 1/2 there is only one component *)
apply wf_incl with (rest P (rdp_step (axiom (fun v u : term => comp (u, v) 0)) R)).
intros s t [K [As At]]; split; [ | split; assumption].
inversion K as [f l1 l2 s' H1 H2]; subst.
inversion H2 as [t1 t2 sigma H3 H4 H5]; subst.
constructor 1 with l2.
assumption.
rewrite <- H5; apply instance.
rewrite <- comp_def_on_dps in H3.
destruct H3 as [n H3].
assert (H6 := G _ _ H3); inversion H6; subst n; assumption.
apply (W 0).

(* 1/1, there are at least two components, apply the induction hypothesis by merging the components 1 and 2 *)
set (comp' := fun uv m => match m with 0 => comp uv 0 \/ comp uv 1 | S n => comp uv (S m) end).
apply (IHn comp'); clear IHn.
(* 1/4 *)
intros uv uv' H; assert (K := comp_approx _ _ H); unfold comp'.
intros [ | c] [ | c'].
intros _ _; apply le_n.
intros _ _; apply le_O_n.
intros J [J' | J'].
assert (J'' := K _ _ J J'); inversion J''.
apply (le_S_n _ _ (K _ _ J J')).
intros J J'; apply (le_S_n _ _ (K _ _ J J')).
(* 1/3 *)
intros u v; rewrite <- (comp_def_on_dps u v).
unfold comp'; split.
intros [[ | n0] H].
destruct H as [H | H]; [exists 0 | exists 1]; assumption.
exists (S (S n0)); assumption.
intros [[ | [ | n0]] H].
exists 0; left; assumption.
exists 0; right; assumption.
exists (S n0); assumption.
(* 1/2 *)
unfold comp'; intros [u v] [ | n0].
intros _; apply le_O_n.
intro K; apply le_S_n; apply (G _ _ K).

(* 1/1 *)
intros [ | n0].
(* 1/2 The new component 0 (i.e. the union of old components 0 and 1) is well founded *)
apply wf_incl with (union _ (rest P (rdp_step (axiom (fun v u : term => comp (u, v) 1)) R))
                                   (rest P (rdp_step (axiom (fun v u : term => comp (u, v) 0)) R))).
intros s t [K [As At]];
inversion K as [f l1 l2 s' H1 H2]; subst;
inversion H2 as [t1 t2 sigma H3 H4 H5]; subst.
unfold comp' in H3; destruct H3 as [H3 | H3].
right; split; [ | split; assumption].
constructor 1 with l2.
assumption.
rewrite <- H5; constructor; assumption.
left; split; [ | split; assumption].
constructor 1 with l2.
assumption.
rewrite <- H5; constructor; assumption.
clear comp'.
intro a; rewrite <- (acc_union_alt _ (W 1)).
intros t _; clear a.
pattern t; apply (well_founded_ind (W 0)); clear t; intro t.
set (R0 := rest P (rdp_step (axiom (fun v u : term => comp (u, v) 0)) R)) in *.
set (R1 := rest P (rdp_step (axiom (fun v u : term => comp (u, v) 1)) R)) in *.
intros IH0.
rewrite accR2; apply Acc_intro; intros s H; rewrite <- accR2.
inversion H as [a1 a3 a5 H13 H35]; clear H; subst s t.
inversion H35 as [a3' a4 a5' H34 H45]; subst a3' a5'.
inversion H34 as [a34 | a3' a4' K34]; clear H34.
subst a3 a4.
apply Acc_inv with a34; [ apply IH0 | ]; assumption.
subst a3' a4'.
assert (H : exists a, R1 a a4).
rewrite trans_clos_trans_clos_alt in K34; inversion K34 as [a3' a4' H34 | a3' a a4' H3 H4]; clear K34; subst a3' a4'.
exists a3; assumption.
exists a; assumption.
destruct H as [a H]; apply False_rect.
destruct H45 as [H45 _]; destruct H as [H _].
inversion H45 as [f l5 l4 t4 H5 H4]; subst a4 a5; inversion H4 as [v4 u4 sigma4]; subst t4.
inversion H as [g k4 l t K4 K]; subst a; inversion K as [v u sigma]; subst t.
assert (C : are_connected dpR R (u,v) (u4,v4)).
exists sigma4; exists sigma.
split.
rewrite <- comp_def_on_dps; exists 0; assumption.
split.
rewrite <- comp_def_on_dps; exists 1; assumption.
rewrite H7; rewrite <- H3; split; trivial.
assert (Abs := comp_approx _ _ C _ _ H1 H0); inversion Abs.
(* 1/1 The new component n+1 (i.e. the old component n+2) is well founded *)
apply wf_incl with (rest P (rdp_step (axiom (fun v u : term => comp (u, v) (S (S n0)))) R)).
intros s t [K [As At]]; split; [ | split; assumption].
inversion K as [f l1 l2 s' H1 H2]; subst.
inversion H2 as [t1 t2 sigma H3 H4 H5]; subst.
constructor 1 with l2; trivial.
apply W.
Qed.

Inductive lex o1 lo1 o2 : relation term :=
  | Comp1 : forall s t, o1 s t -> lex o1 lo1 o2 s t
  | Comp2 : forall s t, lo1 s t -> o2 s t -> lex o1 lo1 o2 s t.

Lemma wf_lex :
  forall (o1 lo1 o2 : relation term), (forall t1 t2 t3, o1 t1 t2 -> lo1 t2 t3 -> o1 t1 t3) ->
  well_founded o1 -> well_founded o2 -> well_founded (lex o1 lo1 o2).
Proof.
intros o1 lo1 o2 Transo W1 W2.
intro t; apply (well_founded_ind W1); clear t.
intro t; pattern t; apply (well_founded_ind W2); clear t.
intros t IH2 IH1; apply Acc_intro.
intros s H; inversion H as [u1 u2 K | u1 u2 K1 K2]; subst.
apply IH1; assumption.
apply IH2.
assumption.
intros u K3; apply IH1; apply Transo with s; assumption.
Defined.

Lemma remove_edge :
  forall (dpR R : relation term) P u0 v0 (lo so : relation term),
  (forall t, lo t t) ->
  (forall t1 t2 t3, lo t1 t2 -> lo t2 t3 -> lo t1 t3) ->
  (forall t1 t2 t3, so t1 t2 -> lo t2 t3 -> so t1 t3) ->
  well_founded so ->
  (forall s t, one_step R s t -> lo s t) ->
  (forall u v, dpR v u -> forall sigma, lo (apply_subst sigma v) (apply_subst sigma u)) ->
  (forall sigma, so  (apply_subst sigma v0) (apply_subst sigma u0)) ->
  well_founded  (rest P (rdp_step (axiom dpR) R)) ->
  well_founded  (rest P (rdp_step (axiom (union _ (fun s t => (s,t) = (v0,u0)) dpR)) R)).
Proof.
intros dpR R P u0 v0 lo so lo_refl lo_trans Transo Wo Hlo Hlo' Hso W.
assert (WW := wf_lex _ _ _ Transo Wo W).
intro t; apply (well_founded_ind WW); clear t.
intros t IH; apply Acc_intro; intros s H; apply IH; clear WW IH.
destruct H as [H [Ps Pt]].
inversion H as [f l1 l2 v K1 K2]; clear H; subst.
inversion K2 as [v u sigma [K3 | K3]]; clear K2; subst.
injection K3; clear K3; intros; subst u v.
left; apply Transo with (Term f l2).
rewrite <- H0; apply Hso.
inversion K1 as [l | k1 k2 K]; clear K1; subst.
apply lo_refl.
clear Pt H0; induction K as [k1 k2 K | k1 k2 k3 K1 K2].
apply Hlo; apply in_context; assumption.
apply lo_trans with (Term f k2); [apply Hlo; apply in_context | ]; assumption.
right.
apply lo_trans with (Term f l2).
rewrite <- H0; apply Hlo'; assumption.
inversion K1 as [l | k1 k2 K]; clear K1; subst.
apply lo_refl.
clear Pt H0; induction K as [k1 k2 K | k1 k2 k3 K1 K2].
apply Hlo; apply in_context; assumption.
apply lo_trans with (Term f k2); [apply Hlo; apply in_context | ]; assumption.
split; [ constructor 1 with l2; [ | rewrite <- H0; apply instance] | split]; assumption.
Qed.

End MakeIGDP.

author: fblanqui

repo: color

save_path: github-repos/coq/fblanqui-color


text:
From BY.Hierarchy Require Import Definitions Magma.
From stdpp Require Import list.

Local Open Scope mag_scope.
Section SemiGroup.

  Local Open Scope mag_scope.
  Class SemiGroup A `{Equiv A, Op1 A} :=
    {
      sg_setoid :> Setoid A;
      sg_proper :> Proper ((≡) ==> (≡) ==> (≡)) (∘);
      sg_assoc :> Assoc (≡) (∘)
    }.

End SemiGroup.

Section __.

  Context `{SemiGroup A}.

  Local Instance : Magma A. sub_class_tac. Qed.

  Instance quot_sg (rel : relation A) `{!MagmaCongruence rel} `{subrelation A (≡) rel} : @SemiGroup _ rel _.
  Proof. repeat split; try apply _; cbv; intros; apply is_subrelation; eapply assoc; exact _. Qed.

End __.

author: bshvass

repo: by-inversion

save_path: github-repos/coq/bshvass-by-inversion


text:
(** * BinCoeff.v: Binomial coefficients *)
(** Contributed by David Baelde, 2011 *)

Require Import Arith.
Require Import Omega.

(* begin hide *)
Set Implicit Arguments.

(* end hide *)

(** ** Definition of binomial coefficients *)

Fixpoint comb (k n:nat) {struct n} : nat :=
   match n with O => match k with O => (1%nat) | (S l) => O end
          | (S m) => match k with O => (1%nat)
                            | (S l) => ((comb l m) + (comb k m))%nat
                     end
   end.

(** ** Properties of binomial coefficients *)

Lemma comb_0_n : forall n, comb 0 n = 1%nat.
destruct n; trivial.
Save.

Lemma comb_not_le : forall n k, (S n <= k)%nat -> comb k n = 0%nat.
induction n; destruct k; simpl; try omega; intros.
rewrite (IHn k); auto with zarith.
rewrite (IHn (S k)); auto with zarith.
Save.

Lemma comb_Sn_n : forall n, comb (S n) n = 0%nat.
intro; apply comb_not_le; auto.
Save.

Lemma comb_n_n : forall n, comb n n = 1%nat.
induction n; simpl; auto.
rewrite comb_Sn_n; auto with zarith.
Save.

Lemma comb_1_Sn : forall n, comb 1 (S n) = S n.
induction n; auto.
replace (comb 1 (S (S n))) with ((comb 0 (S n)+comb 1 (S n))%nat); auto.
Save.

Lemma comb_inv : forall n k, (k<=n)%nat -> comb k n = comb (n-k) n.
induction n; destruct k; simpl; auto with zarith; intros.
rewrite comb_Sn_n; rewrite comb_n_n; auto.
assert (Hle : (k<=n)%nat); auto with zarith.
case (le_lt_or_eq k n Hle); intros.
assert (Heq:(n-k)%nat=(S (n-(S k)))); auto with zarith.
pattern ((n-k)%nat) at 1; rewrite Heq.
rewrite (IHn (S k)); auto.
rewrite (IHn k); auto with zarith.
subst.
rewrite comb_Sn_n; rewrite comb_n_n; rewrite <- minus_n_n; trivial.
Save.

Lemma comb_n_Sn : forall n, comb n (S n) = (S n).
intros; transitivity (comb (S n - n) (S n)).
apply comb_inv; auto.
rewrite <- minus_Sn_m; auto.
rewrite <- minus_n_n.
apply comb_1_Sn.
Save.

(* Shortcuts for horizontal (k-axis) and vertical (n-axis) relationships for (comb k n). *)
Notation H := (fun n k => comb (S k) (S n) * (S k) = comb k (S n) * (S n - k)).
Notation V := (fun n k => comb k (S n) * (S n - k) = comb k n * (S n)).

Lemma comb_relations : forall n k, H n k /\ V n k.
Proof.
  intro n; induction n; intros.

  (* Case split for the base case: k = 0, 1 or >n. *)
  destruct k; [ auto | destruct k; auto ].

  (* We first treat the "illegal" cases where k>=n+2. *)
  destruct (lt_eq_lt_dec k (S (S n))) as [ [ Lt_k_SSn | Eq_k_SSn ] | Gt_k_SSn ].
  (* k=n+2 *)
  Focus 2.
  rewrite Eq_k_SSn.
  rewrite comb_n_n; repeat rewrite comb_Sn_n;
  repeat rewrite minus_diag; auto with arith.
  (* k>n+2 *)
  Focus 2.
  do 3 (rewrite comb_not_le; auto with arith).

  (* First prove V, then use it to derive H. *)
  assert (V (S n) k) as VSnk.
  destruct k.
  rewrite comb_0_n; auto with arith.
  change (comb (S k) (S (S n))) with (comb k (S n) + comb (S k) (S n)).
  rewrite mult_plus_distr_r.
  assert (H n k) as Hnk.
  elim (IHn k); trivial.
  change (S (S n) - S k) with (S n - k).
  rewrite <- Hnk.
  rewrite <- mult_plus_distr_l.
  replace (S k + (S n - k)) with (S (S n)).
  reflexivity.
  rewrite plus_Sn_m.
  rewrite <- (le_plus_minus k (S n)) by (apply lt_le_weak; auto with arith).
  reflexivity.

  split; try exact VSnk.

  change (comb (S k) (S (S n))) with (comb k (S n) + comb (S k) (S n)).
  rewrite mult_plus_distr_r.
  assert (H n k) as Hnk.
  elim (IHn k); trivial.
  rewrite Hnk.
  rewrite <- mult_plus_distr_l.
  replace (S k + (S n - k)) with (S (S n)).
  rewrite <- VSnk.
  reflexivity.
  rewrite plus_Sn_m.
  rewrite <- (le_plus_minus k (S n)) by (auto with arith).
  reflexivity.
Qed.

Lemma comb_incr_n : forall n k, comb k (S n) * (S n - k) = comb k n * (S n).
Proof.
  intros.
  elim (comb_relations n k).
  trivial.
Qed.

Lemma comb_incr_k : forall n k, comb (S k) (S n) * (S k) = comb k (S n) * (S n - k).
Proof.
  intros.
  elim (comb_relations n k).
  trivial.
Qed.

Lemma comb_fact : forall n k, k<=n -> comb k n * fact k * fact (n-k) = fact n.
Proof.
  (* We iterate Sk_k (rather than Sn_n) hence we proceed by induction on k. *)
  intros n k; induction k.
  (* Base case. *)
  intros _.
  rewrite comb_0_n; simpl fact; simpl mult;
  rewrite <- minus_n_O; rewrite <- plus_n_O; reflexivity.
  (* Successor. *)
  intro.
  change (fact (S k)) with (S k * fact k).
  destruct n.
    (* n can't be 0 *)
    elim (le_Sn_O _ H).
    (* n := S n, we can apply Sk_k *)
    rewrite mult_assoc. rewrite comb_incr_k.
    change (S n - S k) with (n-k).
    rewrite <- minus_Sn_m; try omega.
    repeat rewrite <- mult_assoc.
    rewrite (mult_comm (fact k)).
    rewrite (mult_assoc (S (n-k))).
    change ((S (n - k)) * fact (n - k)) with (fact (S (n - k))).
    rewrite minus_Sn_m; try omega.
    rewrite <- IHk; try omega.
    repeat rewrite <- mult_assoc.
    auto with arith.
Qed.

Lemma comb_le_0_lt : forall k n, k <= n -> 0 < comb k n.
Proof.
  intros.
  elim (zerop (comb k n)); intros.
  assert (comb k n * fact k * fact (n-k) = 0)%nat.
  rewrite a; auto with arith.
  rewrite (comb_fact H) in H0.
  assert (0<0).
  rewrite <- H0 at 2.
  exact (lt_O_fact n).
  inversion H1.
  auto.
Qed.

Lemma mult_simpl_right : forall m n p, 0 < p -> m * p = n * p -> m = n.
Proof.
  intros.
  assert (m<n \/ n<m \/ m=n) as [H1|[H1|H1]] by omega.
  exfalso; assert (m * p < n * p);  [|omega].
  apply mult_lt_compat_r; assumption.
  exfalso; assert (m * p > n * p); [|omega].
  apply mult_lt_compat_r; assumption.
  assumption.
Qed.

Corollary comb_symmetric : forall k n, k<=n -> comb k n = comb (n-k) n.
Proof.
  intros.
  assert (comb k n * (fact k * fact (n-k)) =
          comb (n-k) n * (fact (n-(n-k)) * fact (n-k))).
    rewrite mult_assoc. rewrite comb_fact; [ | omega ].
    rewrite (mult_comm (fact (n-(n-k)))). rewrite mult_assoc. rewrite comb_fact; [ | omega ].
    reflexivity.
  replace (n-(n-k)) with k in H0 by omega.
  assert (0 < fact k * fact (n - k)) by
    (change 0 with (0 * fact (n-k)); apply mult_lt_compat_r; apply lt_O_fact).
  apply (mult_simpl_right _ _ H1 H0).
Qed.

Lemma mult_lt_compat_l : forall n m p : nat, n < m -> 0 < p -> p * n < p * m.
Proof.
  intros.
  rewrite <- 2!mult_comm with (m:=p).
  apply mult_lt_compat_r; assumption.
Qed.

Lemma comb_monotonic_k : forall k n k', 0<n -> k<=k' -> 2*k'<=n -> comb k n <= comb k' n.
Proof.
  intros k n k' Hn Hkk'; induction Hkk'; intros.
  auto.
  apply le_trans with (comb m n).
  apply IHHkk'.
  omega.
  assert (comb (S m) n * (S m) = comb m n * (n-m)).
    replace n with (S (pred n)) by omega.
    apply comb_incr_k.
  assert (comb m n <= comb (S m) n \/ comb m n > comb (S m) n) by omega.
  destruct H1.
  assumption.
  assert (comb (S m) n * S m < comb m n * (n-m)); [ | omega ].
  transitivity (comb m n * S m).
  apply mult_lt_compat_r; omega.
  apply mult_lt_compat_l; omega.
Qed.

Lemma comb_monotonic_n : forall k n n', k<=n -> n<=n' -> comb k n <= comb k n'.
Proof.
  intros k n n' Hk Hle; induction Hle.
  auto.
  apply le_trans with (comb k m); [ assumption | clear IHHle ].
  assert (comb k m * S m = comb k (S m) * ((S m) - k)).
    rewrite comb_incr_n; reflexivity.
  (* Ab absurdo *)
  assert (comb k m <= comb k (S m) \/ comb k (S m) < comb k m) by omega;
    destruct H0; try assumption.
  assert (comb k (S m) * (S m - k) < comb k m * S m); [ | omega ].
  apply le_lt_trans with (m:= comb k (S m) * S m).
  apply mult_le_compat_l; omega.
  apply mult_lt_compat_r; omega.
Qed.

Lemma comb_monotonic :
  forall k n k' n', 0<n -> k<=n -> k<=k' -> 2*k'<=n' -> n<=n' -> comb k n <= comb k' n'.
Proof.
  intros.
  apply le_trans with (comb k n').
  apply comb_monotonic_n; omega.
  apply comb_monotonic_k; omega.
Qed.

Lemma comb_max_half : forall k n, comb k n <= comb (Div2.div2 n) n.
Proof.
  intros.
  (* Eliminate the case where n = 0 *)
  destruct n.
    destruct k; simpl; auto.
  (* Eliminate the case where k > n *)
  assert (k > S n \/ k <= S n) by omega.
  destruct H as [ H | H ].
  rewrite comb_not_le by try omega.
  apply lt_le_weak.
  apply comb_le_0_lt.
  apply lt_le_weak.
  apply Div2.lt_div2; omega.
  (* Treat the case where k <= n/2 *)
  assert (forall k, k <= Div2.div2 (S n) -> comb k (S n) <= comb (Div2.div2 (S n)) (S n)).
    intros.
    apply comb_monotonic_k; try omega.
    replace (2 * Div2.div2 (S n)) with (Div2.double (Div2.div2 (S n)))
      by (unfold Div2.double; omega).
    destruct (Even.even_or_odd (S n)) as [ He | Ho ] ;
    [ rewrite <- Div2.even_double with (1:=He); auto |
      apply le_S_n; rewrite <- Div2.odd_double with (1:=Ho); omega ].
  (* By symmetry we can conclude *)
  assert (k <= Div2.div2 (S n) \/ k > Div2.div2 (S n)) by omega.
    (* Immediate if k<=n/2 *)
    destruct H1 as [ H1 | H1 ].
    auto.
    (* Otherwise get back to that case *)
    rewrite comb_inv with (1:=H).
    apply H0.
    assert (S n <= Div2.div2 (S n) + k).
    assert (S n <= S (Div2.double (Div2.div2 (S n)))) by
      (destruct (Even.even_or_odd (S n)) as [ He | Ho ];
       [ apply le_S_n; rewrite <- Div2.even_double with (1:=He); omega |
         apply le_S_n; rewrite <- Div2.odd_double with (1:=Ho); omega ]).
    unfold Div2.double in H2.
    omega.
    omega.
Qed.

author: hivert

repo: Coq-HookLength

save_path: github-repos/coq/hivert-Coq-HookLength


text:
(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import Undecidability.Synthetic.Undecidability.

From Undecidability.MinskyMachines
  Require Import MMA MM2 MMA2_undec MMA2_to_MM2.

From Undecidability.MinskyMachines.Reductions
  Require MM2_HALTING_to_MM2_ZERO_HALTING.

(** ** MM2_HALTING is undecidable *)

Lemma MM2_HALTING_undec : undecidable MM2_HALTING.
Proof.
  apply (undecidability_from_reducibility MMA2_HALTING_undec).
  apply MMA2_MM2_HALTING.
Qed.

Check MM2_HALTING_undec.

Lemma MM2_ZERO_HALTING_undec : undecidable MM2_ZERO_HALTING.
Proof.
  apply (undecidability_from_reducibility MM2_HALTING_undec).
  exact MM2_HALTING_to_MM2_ZERO_HALTING.reduction.
Qed.

Check MM2_ZERO_HALTING_undec.

Lemma MM2_HALTS_ON_ZERO_undec : undecidable MM2_HALTS_ON_ZERO.
Proof.
  apply (undecidability_from_reducibility MMA2_HALTS_ON_ZERO_undec).
  apply MMA2_MM2_HALTS_ON_ZERO.
Qed.

Check MM2_HALTS_ON_ZERO_undec.

author: uds-psl

repo: coq-library-undecidability


text:
From Mon Require Import FiniteProbabilities SPropMonadicStructures
  SpecificationMonads MonadExamples SPropBase.

From Relational Require Import OrderEnrichedCategory
  OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple.

Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_algebra reals distr realsum.
Set Warnings "notation-overridden,ambiguous-paths".

From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings Theta_dens
  Theta_exCP LaxComp FreeProbProg UniformDistrLemmas
  Prelude choice_type StateTransformingLaxMorph RulesStateProb.

Import SPropNotations.
Import Num.Theory.

Local Open Scope ring_scope.

(* general Rules + Rules for uniform distributions over a finite
    family of non-empty finite types *)

Definition Index : Type := positive.

Definition fin_family (i : Index) : finType := [finType of chFin i].

Lemma F_w0 :
  forall (i : Index), fin_family i.
Proof.
  intros i. unfold fin_family. cbn.
  exists 0%N. eapply i.(cond_pos).
Qed.

(* extend the initial parameters for the rules  *)

Definition Uni_W : forall i, SDistr (fin_family i).
  move=> i. apply (@uniform_F (fin_family i)).
  apply F_w0.
Defined.

Definition Uni_W' : forall i, SDistr( chFin i) := Uni_W.

Definition Fail_Unit : SDistr chUnit.
  exact dnull.
Defined.

#[local] Definition FrStP := @FrStP.
(* #[local] Definition θ0 {S} {A} (c : @FrStP S A) := @θ0 S A c. *)
(* #[local] Definition θ_dens {S} {X} := @θ_dens S X. *)

(* Definition inhab (i : positive) : [finType of chFin i]. *)
(* destruct i as [i ipos]. destruct i. *)
(* - cbv in ipos. discriminate. *)
(* - cbn. unshelve econstructor. *)
(*   exact i. auto. *)
(* Defined. *)

(* Uniform distribution over F *)
Definition Uniform_F {i : Index} {S : choiceType} : @FrStP S (fin_family i).
Proof.
  rewrite /=.
  rewrite /ops_StP /ar_StP /fin_family.
  (* pose usd :=  @uniform_F [finType of chFin i] (inhab i). *)
  unshelve eapply ropr.
  - apply op_iota. unshelve econstructor.
    + exact (chFin i).
    + apply Uni_W'.
  - rewrite /=. move=> j. eapply retrFree. assumption.
Defined.

Definition Uniform ( i : Index ) { S : choiceType } { s : S } :=
  θ_dens (θ0 (@Uniform_F i S) s).

Lemma Uniform_eval (i : Index ) {S : choiceType} {s : S} :
  forall (st : S) (w : fin_family i),
    @Uniform i S s (w, st) =
    if st == s then @r (fin_family i) (F_w0 i) else 0.
Proof.
  (* move=> st w. rewrite /Uniform /=. *)
  (* case bb : (st == s). *)
  (* - rewrite  *)
  cbn.
  rewrite /SDistr_bind /SDistr_unit => st w /=.
  rewrite dletE.
  match goal with
  | |- psum ?k = _ =>
    eassert (k = _) as H
  end.
  { extensionality x.
    rewrite dunit1E.
    eassert (((x, s) == (w, st))%:R = (x == w)%:R * (s == st)%:R).
    { destruct (x == w) eqn:e1, (s == st) eqn:e2.
      all: cbn.
      all: cbn in e1.
      all: rewrite ?e1 ?e2.
      all: cbn.
      all: rewrite ?GRing.mulr1 ?GRing.mul0r ?GRing.mulr0.
      all: reflexivity.
    }
    rewrite H.
    rewrite GRing.mulrA.
    rewrite -dunit1E.
    reflexivity.
  }
  rewrite H. clear H.
  rewrite psumZr.
  2:{
    destruct (s == st). all: cbn.
    - apply (@ler01 R).
    - apply Order.POrderTheory.lexx.
  }
  rewrite -dletE.
  rewrite dlet_dunit_id.
  destruct (s == st) eqn:Heq.
  - have Heq' : st == s. apply /eqP. by move /eqP: Heq.
    rewrite Heq'. rewrite GRing.mulr1. reflexivity.
  - have Heq' : st == s = false. apply /eqP. move /eqP: Heq. congruence.
    rewrite Heq'. rewrite GRing.mulr0. reflexivity.
  Unshelve. exact (Real.ringType R).
Qed.

Definition f_dprod { F1 F2: finType } { S1 S2 : choiceType } { w0 : F1 } { w0' : F2 } {s1 : S1 } {s2 : S2}
            (f : F1 -> F2) : (F1 * S1) * (F2 * S2) -> R :=
fun '((w1,st1),(w2, st2)) => if  ((st1 == s1) && (st2 == s2) && ((f w1) == w2)) then (@r F1 w0) else 0.

Lemma item_addr0_mulr :
  forall n x,
    (* @iter R n (+%R x) 0 = x * n%:~R. *)
    @iter R n (+%R x) 0 = x *~ n.
Proof.
  intros n x.
  induction n as [| n ih].
  - cbn. reflexivity.
  - simpl. rewrite ih.
    unfold intmul. rewrite GRing.mulrS. reflexivity.
Qed.

Lemma bijective_isdistr
  {F1 F2 : finType} {w0 : F1} {w0' : F2}
  {S1 S2 : choiceType} {s1 : S1} {s2 : S2}
  {f : F1 -> F2} (f_bij : bijective f) :
  isdistr (@f_dprod F1 F2 S1 S2 w0 w0' s1 s2 f).
Proof.
  rewrite /f_dprod.
  split.
  - move => [[w1 st1] [w2 st2]].
    destruct ((st1 == s1) && (st2 == s2) && (f w1 == w2)) eqn:Heq; auto.
    exact r_nonneg.
  - rewrite /= => J uniq_J.
    rewrite [X in X<=_](bigID [pred j : _ | (j.1.2 == s1) && (j.2.2 == s2) && (f j.1.1 == j.2.1)]) /=.
    lazymatch goal with
    | |- context [ _ + ?x ] =>
      assert (e : x == 0)
    end.
    { rewrite psumr_eq0.
      - apply/allP. intros [[w1 st1] [w2 st2]] h. cbn.
        match goal with
        | |- context [ if ?b then _ else _ ] =>
          destruct b
        end.
        + cbn. reflexivity.
        + cbn. apply/eqP. reflexivity.
      - intros [[w1 st1] [w2 st2]]. cbn. intros h.
        match goal with
        | |- context [ if ?b then _ else _ ] =>
          destruct b
        end.
        1: discriminate.
        auto.
    }
    move: e => /eqP e. rewrite e. clear e.
    rewrite GRing.Theory.addr0.
    erewrite sum_oneq_eq with (G := fun i => r).
    2:{
      intros [[w1 st1] [w2 st2]]. cbn. intros h.
      rewrite h. reflexivity.
    }
    rewrite big_const_seq. cbn.
    match goal with
    | |- context [ count ?p _ ] =>
      set (P := p)
    end.
    pose (J' := [seq p <- J | P p ]).
    assert (e1 : count P J = size J').
    { rewrite size_filter. reflexivity. }
    pose (g := fun i => ((i, s1), (f i, s2))).
    pose (proj := fun (j : F1 * S1 * (F2 * S2)) => let '((i,_),_) := j in i).
    pose (g' := g \o proj).
    pose (J'' := [seq g' j | j <- J' ]).
    assert (e2 : J' = J'').
    { clear - uniq_J.
      subst J' J''. induction J as [| [[w1 st1] [w2 st2]] J ih].
      - cbn. reflexivity.
      - simpl. destruct (P _) eqn:e.
        + simpl. f_equal.
          * unfold P in e. simpl in e.
            move: e => /andP [e /eqP ?]. move: e => /andP [/eqP ? /eqP ?].
            subst. reflexivity.
          * eapply ih. cbn in uniq_J. move: uniq_J => /andP []. auto.
        + eapply ih. cbn in uniq_J. move: uniq_J => /andP []. auto.
    }
    subst g'.
    unfold J'' in e2. rewrite -> map_comp in e2.
    assert (uniq_J' : uniq J').
    { subst J'. apply filter_uniq. auto. }
    pose (I := [seq g i | i <- enum F1]).
    assert (e3 : (size J' <= size I)%N).
    { subst I. rewrite size_map.
      rewrite e2. rewrite size_map.
      eapply uniq_leq_size.
      1:{ rewrite e2 in uniq_J'. apply map_uniq in uniq_J'. auto. }
      intros x h. rewrite mem_enum. reflexivity.
    }
    rewrite -e1 in e3.
    subst I. rewrite size_map in e3.
    rewrite -cardE in e3.
    rewrite item_addr0_mulr.
    eapply Order.POrderTheory.le_trans with (y := @r _ w0 *~ #|F1|).
    + rewrite -mulrzr. rewrite -[X in _<=X]mulrzr.
      rewrite ler_pmul2l.
      * rewrite ler_int. auto.
      * unfold r. apply mulr_gt0.
        -- cbn. rewrite posnum.one_pos_gt0. reflexivity.
        -- rewrite -(@pmulr_rgt0 _ #|F1|%:~R).
            ++ rewrite -(GRing.mul1r (#|F1|%:~R / #|F1|%:~R)).
              rewrite GRing.mulrA.
              rewrite GRing.Theory.mulfK.
              ** rewrite posnum.one_pos_gt0. reflexivity.
              ** unshelve eapply card_non_zero. auto.
            ++ eapply fintype0 in w0 as h.
              destruct #|F1| eqn:e. 1: contradiction.
              rewrite ltr0n. reflexivity.
    + unfold r. rewrite -[X in X <= _]mulrzr. rewrite GRing.div1r.
      erewrite <- GRing.mulr1. rewrite -GRing.mulrA.
      rewrite GRing.Theory.mulKf.
      * auto.
      * unshelve eapply card_non_zero. auto.
Qed.

Definition UniformFsq_f { F1 F2 : finType} { w0 : F1 } { w0' : F2 }
                        { S1 S2 : choiceType } { s1 : S1 } { s2 : S2 }
                        {f : F1 -> F2} (f_bij : bijective f):
  SDistr (ChoiceAsOrd.F_choice_prod ⟨ ChoiceAsOrd.F_choice_prod ⟨ Finite.choiceType F1 , S1 ⟩ ,
                                    ChoiceAsOrd.F_choice_prod ⟨ Finite.choiceType F2 , S2 ⟩ ⟩ ).
Proof.
  unshelve eapply mkdistr.
  1:{
    exact: (@f_dprod F1 F2 S1 S2 w0 w0' s1 s2 f).
  }
  by apply: bijective_isdistr.
Defined.

Definition UniformSQ { i j : Index } { S1 S2 : choiceType } (s1 : S1) (s2 : S2)
                      { f : fin_family i -> fin_family j } (f_bij : bijective f) :=
  @UniformFsq_f (fin_family i) (fin_family j) (F_w0 i) (F_w0 j) S1 S2 s1 s2 f f_bij.

Lemma bij_same_r { F1 F2 : finType } { w0 : F1 } { w0' : F2 } { f : F1 -> F2 }
      ( bij_f : bijective f ) : @r F1 w0 = @r F2 w0'.
Proof.
  unfold r. f_equal. f_equal. f_equal.
  erewrite <- on_card_preimset with (f := f).
  2:{
    destruct bij_f as [g hfg hgf].
    exists g.
    - intros x hx. apply hfg.
    - intros x hx. apply hgf.
  }
  rewrite cardsT. reflexivity.
Qed.

Lemma UniformSQ_f_coupling { i j : Index}
                            { S1 S2 : choiceType } { s1 : S1 } { s2 : S2 }
                            { f : fin_family i -> fin_family j } (f_bij : bijective f):
  coupling (UniformSQ s1 s2 f_bij) (@Uniform i S1 s1) (@Uniform j S2 s2).
Proof.
  destruct f_bij as [f_inv Kf1 Kf2].
  rewrite /UniformFsq_f /f_dprod.
  split; apply: distr_ext; rewrite /=.
  - move => [w1 st1].
    rewrite /lmg dfstE /mkdistr psum_sum /=.
    rewrite (sum_seq1 ((f w1), s2)).
    by rewrite !refl_true !Bool.andb_true_r Uniform_eval.
    move => [w2 st2] /= H.
    have Hs : (st2 = s2).
    { destruct (st2 == s2) eqn:Heq;  apply /eqP; rewrite Heq; auto.
      exfalso. rewrite Bool.andb_false_r Bool.andb_false_l in H. by move /eqP : H.  }
    have Hf : (f w1 = w2).
    { destruct (f w1 == w2) eqn:Heq; apply /eqP; rewrite Heq; auto.
      rewrite Bool.andb_false_r in H. by move /eqP: H. }
      by rewrite Hs Hf.
    move => [w2 st2] /=.
    destruct ((st1 == s1) && (st2 == s2) && (f w1 == w2)); auto.
    exact: r_nonneg.
  - move => [w2 st2].
    rewrite /rmg dsndE /mkdistr psum_sum /=.
    rewrite (sum_seq1 ((f_inv w2), s1)).
    have Hf: (f (f_inv w2) = w2) by apply: (Kf2 w2).
    have Hs: s1 == s1 by apply /eqP.
    rewrite Hf Hs /= refl_true Bool.andb_true_r Uniform_eval.
    rewrite (@bij_same_r (fin_family i) (fin_family j) (F_w0 i) w2 f).
    reflexivity.
    by exists f_inv.
    move => [w1 st1] /= Hneq.
    have [Hfoo1 Hfoo2] : s1 = st1 /\ f w1 = w2.
    { destruct ((st1 == s1) && (f w1 == w2)) eqn: Heq.
      move /andP : Heq. move => [H1 H2].
      split; by [move /eqP : H1 | move /eqP : H2].
      exfalso. move /eqP: Hneq. rewrite Bool.andb_comm in Heq.
      by rewrite Bool.andb_comm Bool.andb_assoc Heq Bool.andb_false_l. }
    subst.
    by rewrite Kf1 refl_true.
    move => [w1 st1] /=. destruct ((st1 == s1) && (st2 == s2) && (f w1 == w2)); auto.
    exact: r_nonneg.
Qed.

Import RSemanticNotation.
#[local] Open Scope rsemantic_scope.

Theorem Uniform_bij_rule { i j : Index } { S1 S2 : choiceType }
                          { f : fin_family i -> fin_family j } (f_bij : bijective f)
                          (P : S1 * S2 -> Prop) :
  ⊨ ⦃ P ⦄ (@Uniform_F i S1) ≈ (@Uniform_F j S2) ⦃ fun '(w1, s1) '(w2, s2) => P (s1, s2) /\ (f w1 == w2) ⦄.
Proof.
  move => [s1 s2] /=.
  move => π /= [H11 H2].
  exists (UniformSQ s1 s2 f_bij).
  split.
  - by apply: UniformSQ_f_coupling.
  - rewrite /UniformSQ.
    move => [w1 st1] [w2 st2] H. apply: H2.
    rewrite /UniformFsq_f /= in H.
    have hfoo1 : (st1 == s1).
    { destruct (st1 == s1) eqn:Heq; auto.
      by rewrite Bool.andb_false_l  Order.POrderTheory.ltxx in H. }
    have hfoo2 : (st2 == s2).
    { destruct (st2 == s2) eqn:Heq; auto.
      by rewrite Bool.andb_false_r Order.POrderTheory.ltxx in H. }
    have hfoo3 : (f w1 == w2).
    { destruct (f w1 == w2) eqn:Heq; auto.
      by rewrite Bool.andb_false_r  Order.POrderTheory.ltxx in H. }
    move /eqP : hfoo1. move /eqP : hfoo2. move /eqP : hfoo3.
    move => hfoo3 hfoo2 hfoo1. subst.
    split; [assumption |  by rewrite refl_true ].
Qed.

Export RSPNotation.

(*CA: probably not necessary *)
(* Theorem Uniform_bij_rule_sq { i1 i2 j1 j2 : Index } { S1 S2 : choiceType } *)
(*         { f1 : fin_family i1 -> fin_family j1 } (f1_bij : bijective f1) *)
(*         { f2 : fin_family i2 -> fin_family j2 } (f2_bij : bijective f2) *)
(*         (P : S1 * S2 -> Prop) : *)
(*   ⊨ ⦃ P ⦄ ( ( A <- (A <- (@Uniform_F i1 S1) ;; @retrFree _ _ _ A) ;; *)
(*              (B <- (B <- (@Uniform_F i2 S1) ;; @retrFree _ _ _ B) ;; *)
(*              @retrFree _ _ _ (A, B) ))) *)

(*                 ≈ *)
(*           (( A <- (A <- (@Uniform_F j1 S2) ;; @retrFree _ _ _ A) ;; *)
(*            (B <- (B <- (@Uniform_F j2 S2) ;; @retrFree _ _ _ B) ;; *)
(*            @retrFree _ _ _ (A, B) ))) *)
(*        ⦃ fun '((A1, B1), s1) '((A2, B2), s2) => P (s1, s2) /\ (f1 A1 == A2) /\ (f2 B1 == B2) ⦄. *)
(* Proof. *)
(*   unshelve apply: seq_rule. *)
(*   { move => [A1 s1] [A2 s2]. exact: (P (s1, s2) /\ (f1 A1 == A2)). } *)
(*   apply: Uniform_bij_rule. assumption. *)
(*   move => A1 A2. *)
(*   unshelve apply: seq_rule.   *)
(*   { move => [B1 s1] [B2 s2]. exact: ((P (s1, s2) /\ (f1 A1 == A2) ) /\ (f2 B1 == B2)). } *)
(*   simpl.     *)
(*   apply: Uniform_bij_rule f2_bij (fun '(s1,s2) => P (s1, s2) /\ (f1 A1 == A2)). *)
(*   move => B1 B2. *)
(*   simpl.  *)
(*   apply: pre_hypothesis_rule => s1 s2 [[HP H1] H2]. simpl in HP.  *)
(*   move /eqP: H1. move /eqP: H2. move => H2 H1. subst.  *)
(*   unshelve apply: post_weaken_rule. *)
(*   { move => [[A B] st1] [[A' B'] st2]. *)
(*     exact: ((st1 , st2) = (s1, s2) /\ (f1 A, f2 B) = (A', B') ). } *)
(*   simpl. rewrite /fromPrePost.  Check ret_rule (A1,B1) (f1 A1, f2 B1).  *)
(*   admit.  *)
(*   simpl.   *)
(*   move => [[a1 b1] st1] [[a2 b2] st2] [H1 [H2 H3]]. subst. *)
(*   rewrite H1.  *)
(*   split; auto.  *)
(*   Admitted.  *)

Definition Fail { S : choiceType } : FrStP S chUnit.
Proof.
  unshelve eapply ropr.
    apply op_iota. econstructor. exact Fail_Unit.
  move=> _ /=. eapply retrFree. easy.
Defined.

Definition Assert {S : choiceType} (b : bool) : FrStP S chUnit.
Proof.
  destruct b.
  - apply retrFree.
    exact Datatypes.tt.
  - exact Fail.
Defined.

Lemma destruct_pair_eq {R : ringType} {A B : eqType} {a b : A} {c d : B}
  : ((a, c) == (b, d))%:R = (a == b)%:R * (c == d)%:R :> R.
Proof.
  destruct (a == b) eqn:ab, (c == d) eqn:cd.
  all: cbn; rewrite ab cd /=; try rewrite GRing.mulr1; try rewrite GRing.mulr0; reflexivity.
Qed.

Theorem assert_rule { S1 S2 : choiceType }  (b b' : bool) :
  ⊨ ⦃ fun (_ : S1 * S2) => b = b' ⦄ (Assert b) ≈ (Assert b') ⦃ fun _ _ => b = true /\ b' = true ⦄.
Proof.
  intros [s1 s2].
  hnf. intros post. hnf in *.
  cbv in post. intros H.
  cbv in H. destruct H as [Hpre K].
  simpl.
  destruct b, b'.
  all: simpl in *.
  - exists (SDistr_unit _ ((Datatypes.tt, s1), (Datatypes.tt, s2))).
    split.
    + unfold coupling.
      split.
      * unfold lmg. apply distr_ext.
        move => x0. unfold SDistr_unit, dfst.
        rewrite dlet_unit. reflexivity.
      * unfold rmg. apply distr_ext.
        move => x0. unfold SDistr_unit, dsnd.
        rewrite dlet_unit. reflexivity.
    + auto.
  - discriminate.
  - discriminate.
  - exists dnull.
    split.
    + unfold coupling.
      split.
      * unfold SDistr_bind.
        unfold lmg. apply distr_ext.
        move => x0. rewrite !dlet_null.
        reflexivity.
      * unfold SDistr_bind.
        unfold rmg. apply distr_ext.
        move => x0. rewrite !dlet_null.
        reflexivity.
    + intros [a1 s1'] [a2 s2'].
      rewrite dnullE.
      rewrite Order.POrderTheory.ltxx.
      auto.
Qed.

Theorem assert_rule_left { S1 S2 : choiceType }  (b : bool) :
  ⊨ ⦃ fun (_ : S1 * S2) => b = true ⦄ (Assert b) ≈ (retF Datatypes.tt) ⦃ fun _ _ => b = true ⦄.
Proof.
  intros [s1 s2].
  hnf. intros post. hnf in *.
  cbv in post. intros H.
  cbv in H. destruct H as [Hpre K].
  simpl.
  destruct b.
  all: simpl in *.
  - exists (SDistr_unit _ ((Datatypes.tt, s1), (Datatypes.tt, s2))).
    split.
    + unfold coupling.
      split.
      * unfold lmg. apply distr_ext.
        move => x0. unfold SDistr_unit, dfst.
        rewrite dlet_unit. reflexivity.
      * unfold rmg. apply distr_ext.
        move => x0. unfold SDistr_unit, dsnd.
        rewrite dlet_unit. reflexivity.
    + auto.
  - discriminate.
Qed.

Theorem assert_rule_right { S1 S2 : choiceType }  (b : bool) :
  ⊨ ⦃ fun (_ : S1 * S2) => b = true ⦄ (retF Datatypes.tt) ≈ (Assert b) ⦃ fun _ _ => b = true ⦄.
Proof.
  intros [s1 s2].
  hnf. intros post. hnf in *.
  cbv in post. intros H.
  cbv in H. destruct H as [Hpre K].
  simpl.
  destruct b.
  all: simpl in *.
  - exists (SDistr_unit _ ((Datatypes.tt, s1), (Datatypes.tt, s2))).
    split.
    + unfold coupling.
      split.
      * unfold lmg. apply distr_ext.
        move => x0. unfold SDistr_unit, dfst.
        rewrite dlet_unit. reflexivity.
      * unfold rmg. apply distr_ext.
        move => x0. unfold SDistr_unit, dsnd.
        rewrite dlet_unit. reflexivity.
    + auto.
  - discriminate.
Qed.

author: SSProve

repo: ssprove

save_path: github-repos/coq/SSProve-ssprove


text:
From Coqprime Require Import PocklingtonRefl.
Local Open Scope positive_scope.

Lemma primo75:
  prime  104532018694100461->
  prime  378514307375051614573669.
Proof.
intro H.
apply (Pocklington_refl
     (Ell_certif
      378514307375051614573669
      3621037
      ((104532018694100461,1)::nil)
      0
      47250
      15
      225)
     ((Proof_certif _ H) :: nil)).
native_cast_no_check (refl_equal true).
Time Qed.

author: mukeshtiwari


text:
(* This library defines some notions that involve functions and order,
   such as the property of being monotonic. *)

Set Implicit Arguments.
Require Import Coq.Classes.Morphisms Coq.micromega.Lia.
From TLC Require Import LibTactics.

(* -------------------------------------------------------------------------- *)

(* Definitions. *)

(* [within okA okB f] holds iff [f] maps [okA] into [okB]. *)

Definition within A B (okA : A -> Prop) (okB : B -> Prop) (f : A -> B) :=
  forall a,
  okA a ->
  okB (f a).

Definition preserves A (okA : A -> Prop) (f : A -> A) :=
  within okA okA f.

(* [monotonic leA leB f] holds iff [f] is monotonic with respect to
   the relations [leA] and [leB], i.e., [f] maps [leA] to [leB]. *)

Definition monotonic A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :=
  forall a1 a2,
  leA a1 a2 ->
  leB (f a1) (f a2).

(* [inverse_monotonic leA leB f] holds iff [f^-1] maps [leB] to [leA]. *)

Definition inverse_monotonic A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :=
  forall a1 a2,
  leB (f a1) (f a2) ->
  leA a1 a2.

(* [inflationary okA leA] holds iff [a] is less than [f a], with
   respect to the relation [leA], and for every [a] in [okA]. *)

Definition inflationary A (okA : A -> Prop) (leA : A -> A -> Prop) (f : A -> A) :=
  forall a,
  okA a ->
  leA a (f a).

(* If [leB] is a relation on [B], then [pointwise okA leB] is a relation
   on [A -> B]. *)

Definition pointwise A B (okA : A -> Prop) (leB : B -> B -> Prop) (f g : A -> B) :=
  forall a,
  okA a ->
  leB (f a) (g a).

(* -------------------------------------------------------------------------- *)

(* If [f] is monotonic, then rewriting in the argument of [f] is permitted. *)

(* Note: in order for [rewrite] to work properly, the lemmas that are able to
   prove [monotonic] assertions should be added to [typeclass_instances]. *)

(* TEMPORARY maybe this should be the *definition* of [monotonic] *)

Program Instance monotonic_Proper
  A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :
  monotonic leA leB f -> Proper (leA ++> leB) f.

(* -------------------------------------------------------------------------- *)

(* Letting [eauto] exploit [monotonic] and [inverse_monotonic]. *)

Lemma use_monotonic:
  forall B (leB : B -> B -> Prop) A (leA : A -> A -> Prop) (f : A -> B),
  monotonic leA leB f ->
  forall a1 a2,
  leA a1 a2 ->
  leB (f a1) (f a2).
Proof using.
  unfold monotonic. eauto.
Qed.

(* This variant is useful when the function has two arguments and one
   wishes to exploit monotonicity in the first argument. *)

Lemma use_monotonic_2:
  forall B (leB : B -> B -> Prop) A (leA : A -> A -> Prop) C (f : A -> C -> B) a1 a2 c,
  monotonic leA leB (fun a => f a c) ->
  leA a1 a2 ->
  leB (f a1 c) (f a2 c).
Proof using.
  unfold monotonic. eauto.
Qed.

Lemma use_inverse_monotonic:
  forall A (leA : A -> A -> Prop) B (leB : B -> B -> Prop) (f : A -> B),
  inverse_monotonic leA leB f ->
  forall a1 a2,
  leB (f a1) (f a2) ->
  leA a1 a2.
Proof using.
  unfold inverse_monotonic. eauto.
Qed.

(* It seems that these lemmas can be used as a hint only if we pick a
   specific instance of the ordering relation that appears in the
   conclusion. Furthermore, picking a specific instance of the
   ordering relation that appears in the premise can help apply
   [lia] to the premise. *)

Hint Resolve (@use_monotonic nat le nat le) (@use_monotonic nat lt nat lt)
: monotonic typeclass_instances.

Hint Resolve (@use_monotonic_2 nat le nat le) (@use_monotonic_2 nat lt nat lt)
: monotonic typeclass_instances.

Hint Resolve (@use_inverse_monotonic nat le nat le)
(@use_inverse_monotonic nat lt nat lt) : monotonic typeclass_instances.

(* -------------------------------------------------------------------------- *)

(* A little fact. If [f], viewed as a function of [A] into [B -> C], is
   monotonic, then its specialized version [fun a => f a b], which is a
   function of [A] to [C], is monotonic as well. And the converse holds. *)

Lemma monotonic_pointwise_specialize:
  forall A B C leA okB leC (f : A -> B -> C),
  monotonic leA (pointwise okB leC) f ->
  forall b, okB b -> monotonic leA leC (fun a => f a b).
Proof using.
  unfold monotonic, pointwise. auto.
Qed.

Lemma monotonic_pointwise_generalize:
  forall A B C leA (okB : B -> Prop) leC (f : A -> B -> C),
  (forall b, okB b -> monotonic leA leC (fun a => f a b)) ->
  monotonic leA (pointwise okB leC) f.
Proof using.
  unfold monotonic, pointwise. auto.
Qed.

(* -------------------------------------------------------------------------- *)

Require Import Coq.Arith.Arith.

(* The following tactics allow proving implications between inequalities
   by contraposition, while exploiting the fact that the negation of a
   strict inequality is a large inequality. *)

Ltac prove_le_le_by_contraposition :=
  match goal with h: ?a <= ?b |- ?x <= ?y =>
    (destruct (le_gt_dec x y); [ assumption | ]);
    assert (b < a); [ clear h | lia ]
  end.

Ltac prove_lt_lt_by_contraposition :=
  match goal with h: ?a < ?b |- ?x < ?y =>
    (destruct (le_gt_dec y x); [ false | lia ]);
    assert (b <= a); [ clear h | lia ]
  end.

(* If a function of type [nat -> nat] is strictly monotonic, then
   [f x1 <= f x2] implies [x1 <= x2]. The two assertions are in
   fact equivalent, since a strictly monotonic function is a
   fortiori a monotonic function. *)

Lemma monotonic_lt_lt_implies_inverse_monotonic_le_le:
  forall f : nat -> nat,
  monotonic lt lt f ->
  inverse_monotonic le le f.
Proof using.
  intros f ? x y ?. prove_le_le_by_contraposition. eauto.
Qed.

Lemma monotonic_lt_lt_implies_monotonic_le_le:
  forall f : nat -> nat,
  monotonic lt lt f ->
  monotonic le le f.
Proof using.
  introv h. intros x1 x2 ?.
  destruct (eq_nat_dec x1 x2).
    { assert (f x1 = f x2). congruence. lia. }
    { assert (f x1 < f x2). eapply h; lia. lia. }
Qed.

Hint Resolve monotonic_lt_lt_implies_inverse_monotonic_le_le
monotonic_lt_lt_implies_monotonic_le_le : monotonic typeclass_instances.

Goal
  forall f : nat -> nat,
  monotonic lt lt f ->
  forall x1 x2,
  f x1 <= f x2 <-> (* equivalence *)
  x1 <= x2.
Proof using.
  split; eauto with monotonic.
Qed.

(* If a function of type [nat -> nat] is monotonic, then
   [f x1 < f x2] implies [x1 < x2]. The converse is false. *)

Lemma monotonic_le_le_implies_inverse_monotonic_lt_lt:
  forall f : nat -> nat,
  monotonic le le f ->
  inverse_monotonic lt lt f.
Proof using.
  intros f ? x y ?. prove_lt_lt_by_contraposition. eauto.
Qed.

Hint Resolve monotonic_le_le_implies_inverse_monotonic_lt_lt :
monotonic typeclass_instances.

author: Ricagraca

repo: i-splay-tree

save_path: github-repos/coq/Ricagraca-i-splay-tree