text:
(*************************************************************)
(*      This file is distributed under the terms of the      *)
(*      GNU Lesser General Public License Version 2.1        *)
(*************************************************************)
(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
(*************************************************************)

Set Implicit Arguments.

From Bignums Require Import DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv.
From Bignums Require Import DoubleCyclic BigN.
Require Import CyclicAxioms Cyclic31.
Require Import ZArith ZCAux.
Import CyclicAxioms DoubleType DoubleBase.

(* For backward compatibility. The intended value is Set,
   but we use Type when compiling against an old version
   of the standard library. *)
Definition univ_of_cycles : Type.
Proof.
  first [let _ := constr:(word : Set -> nat -> Set) in exact Set | exact Type].
Defined.

Theorem Zpos_pos: forall x, 0 < Zpos x.
red; simpl; auto.
Qed.
Global Hint Resolve Zpos_pos: zarith.

Section Mod_op.

 Variable w : univ_of_cycles.

 Record mod_op : Type := mk_mod_op {
   succ_mod   : w -> w;
   add_mod    : w -> w -> w;
   pred_mod   : w -> w;
   sub_mod    : w -> w -> w;
   mul_mod    : w -> w -> w;
   square_mod : w -> w;
   power_mod  : w -> positive -> w
 }.

 Variable w_op : ZnZ.Ops w.

 Let w_digits      := w_op.(ZnZ.digits).
 Let w_zdigits     := w_op.(ZnZ.zdigits).
 Let w_to_Z        := (@ZnZ.to_Z _ w_op).
 Let w_of_pos      := (@ZnZ.of_pos _ w_op).
 Let w_head0       := (@ZnZ.head0 _ w_op).
 Let w0            := (@ZnZ.zero _ w_op).
 Let w1            := (@ZnZ.one _ w_op).
 Let wBm1          := (@ZnZ.minus_one _ w_op).

 Let wWW           := (@ZnZ.WW _ w_op).
 Let wW0           := (@ZnZ.WO _ w_op).
 Let w0W           := (@ZnZ.OW _ w_op).

 Let w_compare     := (@ZnZ.compare _ w_op).
 Let w_opp_c       := (@ZnZ.opp_c _ w_op).
 Let w_opp         := (@ZnZ.opp _ w_op).
 Let w_opp_carry   := (@ZnZ.opp_carry _ w_op).

 Let w_succ        := (@ZnZ.succ _ w_op).
 Let w_succ_c      := (@ZnZ.succ_c _ w_op).
 Let w_add_c       := (@ZnZ.add_c _ w_op).
 Let w_add_carry_c := (@ZnZ.add_carry_c _ w_op).
 Let w_add         := (@ZnZ.add _ w_op).

 Let w_pred_c      := (@ZnZ.pred_c _ w_op).
 Let w_sub_c       := (@ZnZ.sub_c _ w_op).
 Let w_sub_carry   := (@ZnZ.sub_carry _ w_op).
 Let w_sub_carry_c := (@ZnZ.sub_carry_c _ w_op).
 Let w_sub         := (@ZnZ.sub _ w_op).
 Let w_pred        := (@ZnZ.pred _ w_op).

 Let w_mul_c       := (@ZnZ.mul_c _ w_op).
 Let w_mul         := (@ZnZ.mul _ w_op).
 Let w_square_c    := (@ZnZ.square_c _ w_op).

 Let w_div21       := (@ZnZ.div21 _ w_op).
 Let w_add_mul_div := (@ZnZ.add_mul_div _ w_op).

 Variable b : w.
    (* b should be > 1 *)
 Let n := w_head0 b.

 Let b2n := w_add_mul_div n b w0.

 Let bm1 := w_sub b w1.

 Let mb := w_opp b.

 Let wwb := WW w0 b.

 Let low x := match x with WW _ x => x | W0 => w0 end.

 Let w_add2 x y := match w_add_c x y with
                     C0 n => WW w0 n
                    |C1 n => WW w1 n
                    end.
 Let ww_zdigits := w_add2 w_zdigits w_zdigits.

 Let ww_compare :=
  Eval lazy beta delta [ww_compare] in ww_compare w0 w_compare.

 Let ww_sub :=
 Eval lazy beta delta [ww_sub] in
   ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry.

 Let ww_add_mul_div :=
 Eval lazy beta delta [ww_add_mul_div] in
   ww_add_mul_div w0 wWW wW0 w0W
              ww_compare w_add_mul_div
              ww_sub w_zdigits low (w0W n).

 Let ww_lsl_n :=
   Eval lazy beta delta [ww_add_mul_div] in
    fun ww => ww_add_mul_div  ww W0.

 Let w_lsr_n w :=
     w_add_mul_div (w_sub w_zdigits n) w0 w.

 Open Scope Z_scope.
 Notation "[| x |]" :=
   (@ZnZ.to_Z _ w_op x)  (at level 0, x at level 99).

Notation "[[ x ]]" :=
   (@ww_to_Z _ w_digits w_to_Z x)  (at level 0, x at level 99).

 Section Mod_spec.

   Variable m_op : mod_op.

   Record mod_spec : Prop := mk_mod_spec {
      succ_mod_spec     :
                forall w t, [|w|]= t mod [|b|] ->
                          [|succ_mod m_op w|] = ([|w|] + 1) mod [|b|];
      add_mod_spec      :
            forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] ->
                          [|add_mod m_op w1 w2|] = ([|w1|] + [|w2|]) mod [|b|];
      pred_mod_spec     :
                forall w t, [|w|]= t mod [|b|] ->
                          [|pred_mod m_op w|] = ([|w|] - 1) mod [|b|];
      sub_mod_spec      :
            forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] ->
                          [|sub_mod m_op w1 w2|] = ([|w1|] - [|w2|]) mod [|b|];
      mul_mod_spec      :
            forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] ->
                          [|mul_mod m_op w1 w2|] = ([|w1|] * [|w2|]) mod [|b|];
      square_mod_spec   :
                forall w t, [|w|]= t mod [|b|] ->
                          [|square_mod m_op w|] = ([|w|] * [|w|]) mod [|b|];
      power_mod_spec    :
              forall w t p, [|w|]= t mod [|b|] ->
                          [|power_mod m_op w p|] = (Zpower_pos [|w|] p) mod [|b|]
(*
      shift_spec        :
              forall w p, wf w ->
                          [|shift m_op w p|] = ([|w|] / (Zpower_pos 2 p)) mod [|b|];
      trunc_spec        :
              forall w p, wf w ->
                          [|power_mod m_op w p|] = ([|w1|] mod (Zpower_pos 2 p)) mod [|b|]
*)
    }.

  End Mod_spec.

 Hypothesis b_pos: 1 < [|b|].
 Variable op_spec: ZnZ.Specs w_op.

 Lemma Zpower_n: 0 < 2 ^ [|n|].
 apply Zpower_gt_0; auto with zarith.
 case (ZnZ.spec_to_Z n); auto with zarith.
 Qed.

 Hint Resolve Zpower_n Zmult_lt_0_compat Zpower_gt_0 : core.

 Variable m_op : mod_op.

 Hint Rewrite
    ZnZ.spec_0
    ZnZ.spec_1
    ZnZ.spec_m1
    ZnZ.spec_WW
    ZnZ.spec_opp_c
    ZnZ.spec_opp
    ZnZ.spec_opp_carry
    ZnZ.spec_succ_c
    ZnZ.spec_add_c
    ZnZ.spec_add_carry_c
    ZnZ.spec_add
    ZnZ.spec_pred_c
    ZnZ.spec_sub_c
    ZnZ.spec_sub_carry_c
    ZnZ.spec_sub
    ZnZ.spec_mul_c
    ZnZ.spec_mul
    : w_rewrite.

 Let _succ_mod x :=
  let res :=w_succ x in
  match w_compare res b with
  | Lt => res
  | _ => w0
  end.

 Let split x :=
  match x with
  | W0 => (w0,w0)
  | WW h l => (h,l)
  end.

 Let _w0_is_0: [|w0|] = 0.
 unfold ZnZ.to_Z; rewrite <- ZnZ.spec_0; auto.
 Qed.

 Let _w1_is_1: [|w1|] = 1.
 unfold ZnZ.to_Z; rewrite <-ZnZ.spec_1; simpl; auto.
 Qed.

 Theorem Zmod_plus_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1.
 intros a1 b1 H; rewrite Zplus_mod; auto with zarith.
 rewrite Z_mod_same; try rewrite Zplus_0_r; auto with zarith.
 apply Zmod_mod; auto.
 Qed.

 Theorem Zmod_minus_one: forall a1 b1, 0 < b1 -> (a1 - b1) mod b1 = a1 mod b1.
 intros a1 b1 H; rewrite Zminus_mod; auto with zarith.
 rewrite Z_mod_same; try rewrite Zminus_0_r; auto with zarith.
 apply Zmod_mod; auto.
 Qed.

 Lemma without_c_b: forall w2, [|w2|] < [|b|] ->
    [|w_succ w2|] = [|w2|] + 1.
 intros w2 H.
 unfold w_succ;rewrite ZnZ.spec_succ.
 rewrite Zmod_small;auto.
 assert (HH := ZnZ.spec_to_Z w2).
 assert (HH' := ZnZ.spec_to_Z b);auto with zarith.
 Qed.

 Lemma _succ_mod_spec: forall w t, [|w|]= t mod [|b|] ->
    [|_succ_mod w|] = ([|w|] + 1) mod [|b|].
 intros w2 t H; unfold _succ_mod, w_compare; simpl.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t [|b|]); auto with zarith.
 rewrite ZnZ.spec_compare; case Z.compare_spec; intros H1;
 match goal with H: context[w_succ _] |- _ =>
   generalize H; clear H; rewrite (without_c_b _ F); intros H1;
   auto with zarith
 end.
 rewrite H1, Z_mod_same, _w0_is_0; auto with zarith.
 rewrite Zmod_small; auto with zarith.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 Qed.

 Let _add_mod x y :=
  match w_add_c x y with
  | C0 z =>
    match w_compare z b with
    | Lt => z
    | Eq => w0
    | Gt => w_sub z b
    end
  | C1 z => w_add mb z
  end.

 Lemma _add_mod_correct: forall w1 w2, [|w1|] + [|w2|] < 2 * [|b|] ->
     [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|].
 intros w2 w3; unfold _add_mod, w_compare, w_add_c; intros H.
 match goal with |- context[ZnZ.add_c ?x ?y] =>
   generalize (ZnZ.spec_add_c x y); unfold interp_carry;
   case (ZnZ.add_c x y); autorewrite with w_rewrite
 end; auto with zarith.
 intros w4 H2.
 rewrite ZnZ.spec_compare; case Z.compare_spec; intros H1;
 match goal with H: context[b] |- _ =>
   generalize H; clear H; intros H1; rewrite <-H2;
   auto with zarith
 end.
 rewrite H1, Z_mod_same; auto with zarith.
 rewrite Zmod_small; auto with zarith.
 case (ZnZ.spec_to_Z w4); auto with zarith.
 assert (F1: 0 < [|w4|] - [|b|]); auto with zarith.
 assert (F2: [|w4|] < [|b|] + [|b|]); auto with zarith.
 autorewrite with w_rewrite; auto.
 rewrite (fun x y => Zmod_small (x - y)); auto with zarith.
 rewrite <- (Zmod_minus_one [|w4|]); auto with zarith.
 apply sym_equal; apply Zmod_small; auto with zarith.
 split; auto with zarith.
 apply Z.lt_trans with [|b|]; auto with zarith.
 case (ZnZ.spec_to_Z b); unfold base; auto with zarith.
 rewrite Zmult_1_l; intros w4 H2; rewrite <- H2.
 unfold mb, w_add; rewrite ZnZ.spec_add; auto with zarith.
 assert (F1: [|w4|] < [|b|]).
 assert (F2: base (ZnZ.digits w_op) + [|w4|] < base (ZnZ.digits w_op) + [|b|]);
   auto with zarith.
 rewrite H2.
 apply Z.lt_trans with ([|b|] +[|b|]); auto with zarith.
 apply Zplus_lt_compat_r; auto with zarith.
 case (ZnZ.spec_to_Z b); auto with zarith.
 assert (F2: [|b|] < base (ZnZ.digits w_op) + [|w4|]); auto with zarith.
 apply Z.lt_le_trans with (base (ZnZ.digits w_op)); auto with zarith.
 case (ZnZ.spec_to_Z b); auto with zarith.
 case (ZnZ.spec_to_Z w4); auto with zarith.
 assert (F3: base (ZnZ.digits w_op) + [|w4|] < [|b|] + [|b|]); auto with zarith.
 rewrite <- (fun x => Zmod_minus_one (base x + [|w4|])); auto with zarith.
 rewrite (fun x y => Zmod_small (x - y)); auto with zarith.
 unfold w_opp;rewrite (ZnZ.spec_opp b).
 rewrite <- (fun x => Zmod_plus_one (-x)); auto with zarith.
 rewrite (Zmod_small (- [|b|] + base (ZnZ.digits w_op)));auto with zarith.
 2 : assert (HHH := ZnZ.spec_to_Z b);auto with zarith.
 repeat rewrite Zmod_small; auto with zarith.
 Qed.

 Lemma _add_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
     [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|].
 intros w2 w3 t1 t2 H H1.
 apply _add_mod_correct; auto with zarith.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t1 [|b|]); auto with zarith.
 assert (F': [|w3|] < [|b|]).
 case (Z_mod_lt t2 [|b|]); auto with zarith.
 assert (tmp: forall x, 2 * x = x + x); auto with zarith.
 Qed.

 Let _pred_mod x :=
  match w_compare w0 x with
  | Eq => bm1
  | _ => w_pred x
  end.

 Lemma _pred_mod_spec: forall w t, [|w|] = t mod [|b|] ->
   [|_pred_mod w|] = ([|w|] - 1) mod [|b|].
 intros w2 t H; unfold _pred_mod, w_compare, bm1; simpl.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t [|b|]); auto with zarith.
 rewrite ZnZ.spec_compare; case Z.compare_spec; intros H1;
 match goal with H: context[w2] |- _ =>
   generalize H; clear H; intros H1; autorewrite with w_rewrite;
   auto with zarith
 end; try rewrite _w0_is_0; try rewrite _w1_is_1; auto with zarith.
 rewrite <- H1, _w0_is_0; simpl.
 rewrite <- (Zmod_plus_one (-1)); auto with zarith.
 repeat rewrite Zmod_small; auto with zarith.
 case (ZnZ.spec_to_Z b); auto with zarith.
 unfold w_pred;rewrite ZnZ.spec_pred; auto.
 assert (HHH := ZnZ.spec_to_Z b);repeat rewrite Zmod_small;auto with
 zarith.
 intros;assert (HHH := ZnZ.spec_to_Z w2);auto with zarith.
 Qed.

 Let _sub_mod x y :=
  match w_sub_c x y with
  | C0 z => z
  | C1 z => w_add z b
  end.

 Lemma _sub_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
   [|_sub_mod w1 w2|] = ([|w1|] - [|w2|]) mod [|b|].
 intros w2 w3 t1 t2; unfold _sub_mod, w_compare, w_sub_c; intros H H1.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t1 [|b|]); auto with zarith.
 assert (F': [|w3|] < [|b|]).
 case (Z_mod_lt t2 [|b|]); auto with zarith.
 match goal with |- context[ZnZ.sub_c ?x ?y] =>
   generalize (ZnZ.spec_sub_c x y); unfold interp_carry;
   case (ZnZ.sub_c x y); autorewrite with w_rewrite
 end; auto with zarith.
 intros w4 H2.
 rewrite Zmod_small; auto with zarith.
 split; auto with zarith.
 rewrite <- H2; case (ZnZ.spec_to_Z w4); auto with zarith.
 apply Z.le_lt_trans with [|w2|]; auto with zarith.
 case (ZnZ.spec_to_Z w3); auto with zarith.
 intros w4 H2; rewrite <- H2.
 unfold w_add; rewrite ZnZ.spec_add; auto with zarith.
 case (ZnZ.spec_to_Z w4); intros F1 F2.
 assert (F3: 0 <= - 1 *  base (ZnZ.digits w_op) + [|w4|] + [|b|]); auto with zarith.
 rewrite H2.
 case (ZnZ.spec_to_Z w3); case (ZnZ.spec_to_Z w2); auto with zarith.
 rewrite <- (fun x => Zmod_minus_one ([|w4|] + x)); auto with zarith.
 rewrite <- (fun x y => Zmod_plus_one (-y + x)); auto with zarith.
 repeat rewrite Zmod_small; auto with zarith.
 case (ZnZ.spec_to_Z b); auto with zarith.
 Qed.

 Let _mul_mod x y :=
  let xy := w_mul_c x y in
  match ww_compare xy wwb with
  | Lt => snd (split xy)
  | Eq => w0
  | Gt =>
    let xy2n := ww_lsl_n xy in
    let (h,l) := split xy2n in
    let (q,r) := w_div21 h l b2n in
    w_lsr_n r
  end.

 Theorem high_zero:forall x, [[x]] < base w_digits -> [|fst (split x)|] = 0.
  intros x; case x; simpl; auto.
 intros xh xl H; case (Zle_lt_or_eq 0 [|xh|]); auto with zarith.
 case (ZnZ.spec_to_Z xh); auto with zarith.
 intros H1; contradict H; apply Zle_not_lt.
 assert (HHHH := wB_pos w_digits).
 unfold w_to_Z.
 match goal with |- ?X <= ?Y + ?Z =>
  pattern X at 1; rewrite <- (Zmult_1_l X); auto with zarith;
  apply Z.le_trans with Y; auto with zarith
 end.
 case (ZnZ.spec_to_Z xl); auto with zarith.
 Qed.

 Theorem n_spec: base (ZnZ.digits w_op) / 2 <= 2 ^ [|n|] * [|b|]
                        < base (ZnZ.digits w_op).
 unfold n, w_head0; apply (ZnZ.spec_head0); auto with zarith.
 Qed.

 Theorem b2n_spec: [|b2n|] = 2 ^ [|n|] * [|b|].
 unfold b2n, w_add_mul_div; case n_spec; intros Hp Hp1.
 assert (F1: [|n|] < Zpos (ZnZ.digits w_op)).
 case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto with zarith.
 intros H1; contradict Hp1; apply Zle_not_lt; unfold base.
 apply Z.le_trans with (2 ^ [|n|] * 1); auto with zarith.
 rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith.
 rewrite ZnZ.spec_add_mul_div; auto with zarith.
 rewrite _w0_is_0; rewrite Zdiv_0_l; auto with zarith.
 rewrite Zplus_0_r; rewrite Zmult_comm; apply Zmod_small; auto with zarith.
 Qed.

 Theorem ww_lsl_n_spec: forall w, [[w]] < [|b|] * [|b|] ->
   [[ww_lsl_n w]] = 2 ^ [|n|] * [[w]].
 intros w2 H; unfold ww_lsl_n.
 case n_spec; intros Hp Hp1.
 assert (F0: forall x, 2 * x = x + x) by auto with zarith.
 assert (F1: [|n|] < Zpos (ZnZ.digits w_op)).
 case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]). 2: auto.
 intros H1; contradict Hp1; apply Zle_not_lt; unfold base.
 apply Z.le_trans with (2 ^ [|n|] * 1). 2: auto with zarith.
 rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith.
 assert (F2: [|n|] < Zpos (xO (ZnZ.digits w_op))).
 rewrite (Zpos_xO (ZnZ.digits w_op)). rewrite F0.
 pattern [|n|]; rewrite <- Zplus_0_r.
 apply Zplus_lt_compat; auto with zarith.
 change
  ([[DoubleLift.ww_add_mul_div w0 wWW wW0 w0W
              ww_compare w_add_mul_div
              ww_sub w_zdigits low (w0W n) w2 W0]] = 2 ^ [|n|] * [[w2]]).
 rewrite (DoubleLift.spec_ww_add_mul_div ).
 2: auto with zarith.
 2: apply ZnZ.spec_to_Z; auto.
 2: refine (spec_ww_to_Z _ _ _); auto.
 2: apply ZnZ.spec_to_Z; auto.
 2: apply ZnZ.spec_WW; auto.
 2: apply ZnZ.spec_WO; auto.
 2: apply ZnZ.spec_OW; auto.
 2: refine (spec_ww_compare _ _ _ _ _ _ _); auto.
 2: apply ZnZ.spec_to_Z; auto.
 2: apply ZnZ.spec_compare; auto.
 2: apply ZnZ.spec_add_mul_div; auto.
 2: refine (spec_ww_sub _ _ _ _ _ _ _ _ _ _
                _ _ _ _ _ _ _ _ _ _ _); auto.
 2: apply ZnZ.spec_to_Z; auto.
 2: apply ZnZ.spec_WW; auto.
 2: apply ZnZ.spec_opp_c; auto.
 2: apply ZnZ.spec_opp; auto.
 2: apply ZnZ.spec_opp_carry; auto.
 2: apply ZnZ.spec_sub_c; auto.
 2: apply ZnZ.spec_sub; auto.
 2: apply ZnZ.spec_sub_carry; auto.
 2: apply ZnZ.spec_zdigits; auto.
 replace ([[w0W n]]) with  [|n|].
 change [[W0]] with 0. rewrite Zdiv_0_l; auto with zarith.
 rewrite Zplus_0_r; rewrite Zmod_small; auto with zarith.
 split; auto with zarith.
 case spec_ww_to_Z with (w_digits := w_digits) (w_to_Z := w_to_Z) (x:=w2); auto with zarith.
 apply ZnZ.spec_to_Z; auto.
 apply Z.lt_trans with ([|b|] * [|b|] * 2 ^ [|n|]); auto with zarith.
 apply Zmult_lt_compat_r; auto with zarith.
 rewrite <- Zmult_assoc.
 unfold base; unfold base in Hp.
 unfold ww_digits,w_digits;rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith.
 rewrite Zpower_exp; auto with zarith.
 apply Zmult_lt_compat; auto with zarith.
 case (ZnZ.spec_to_Z b); auto with zarith.
 split; auto with zarith.
 rewrite Zmult_comm; auto with zarith.
 unfold w_digits;auto with zarith.
 generalize (ZnZ.spec_OW n).
 unfold ww_to_Z, w_digits; auto.
 intros x; case x; simpl.
 unfold w_to_Z, w_digits, w0; rewrite ZnZ.spec_0; auto.
 intros w3 w4; rewrite Zplus_comm.
 rewrite Z_mod_plus; auto with zarith.
 rewrite Zmod_small; auto with zarith.
 case (ZnZ.spec_to_Z w4); auto with zarith.
 unfold base; auto with zarith.
 unfold ww_to_Z, w_digits, w_to_Z, w0W; auto.
 rewrite ZnZ.spec_OW; auto with zarith.
 Qed.

 Theorem w_lsr_n_spec: forall w, [|w|] < 2 ^ [|n|] *  [|b|]->
   [|w_lsr_n w|] = [|w|] / 2 ^ [|n|].
 intros w2 H.
 case (ZnZ.spec_to_Z w2); intros U1 U2.
 unfold w_lsr_n, w_add_mul_div.
 rewrite ZnZ.spec_add_mul_div.
 rewrite _w0_is_0; rewrite Zmult_0_l.
 rewrite Zplus_0_l.
 autorewrite with w_rewrite.
 rewrite (fun x y => Zmod_small (x - y)).
 unfold w_zdigits; rewrite ZnZ.spec_zdigits.
 assert (tmp: forall p q, p - (p - q) = q) by (intros; ring).
  rewrite tmp; clear tmp.
 rewrite Zmod_small. reflexivity.
 split. auto with zarith.
 apply Z.le_lt_trans with (2 := U2).
 apply Zdiv_le_upper_bound. auto with zarith.
 apply Z.le_trans with ([|w2|] * (2 ^ 0)).
 simpl Zpower; rewrite Zmult_1_r; reflexivity.
 apply Zmult_le_compat_l. 2: auto with zarith.
 apply Zpower_le_monotone; auto with zarith.
 case (ZnZ.spec_to_Z n); auto with zarith.
 unfold n.
 assert (HH: 0 < [|b|]) by auto with zarith.
 split.
   case (Zle_or_lt [|w_head0 b|] [|w_zdigits|]); auto with zarith.
   unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto; intros H1.
   case (ZnZ.spec_head0 b HH); intros _ H2; contradict H2.
   apply Zle_not_lt; unfold base.
   apply Z.le_trans with (2^[|ZnZ.head0 b|] * 1); auto with zarith.
   rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith.
 unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto.
 apply Z.le_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith.
    case (ZnZ.spec_to_Z (w_head0 b)); auto with zarith.
 unfold base; apply Zpower2_lt_lin; auto with zarith.
 autorewrite with w_rewrite; auto.
 rewrite Zmod_small; auto with zarith.
 unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto with zarith.
 case (ZnZ.spec_to_Z n); auto with zarith.
 unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto.
 split; auto with zarith.
 case (Zle_or_lt [|n|] (Zpos (ZnZ.digits w_op))); auto with zarith; intros H1.
 case (ZnZ.spec_head0 b); auto with zarith; intros _ H2.
 contradict H2; apply Zle_not_lt; auto with zarith.
 unfold base; apply Z.le_trans with (2 ^ [|ZnZ.head0 b|] * 1);
   auto with zarith.
 rewrite Zmult_1_r; unfold base; apply Zpower_le_monotone; auto with zarith.
 apply Z.le_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith.
 case (ZnZ.spec_to_Z n); auto with zarith.
 unfold base; apply Zpower2_lt_lin; auto with zarith.
 Qed.

 Lemma split_correct: forall x, let (xh, xl) := split x in [[WW xh xl]] = [[x]].
 intros x; case x; simpl; unfold w0, w_to_Z;try rewrite ZnZ.spec_0; auto with zarith.
 Qed.

 Lemma _mul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
   [|_mul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|].
 intros w2 w3 t1 t2 H H1; unfold _mul_mod, wwb.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t1 [|b|]); auto with zarith.
 assert (F': [|w3|] < [|b|]).
 case (Z_mod_lt t2 [|b|]); auto with zarith.
 match goal with |- context[ww_compare ?x ?y] =>
   change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y)
 end.
 rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare
    ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare
    (w_mul_c w2 w3) (WW w0 b)).
 case Z.compare_spec; intros H2;
 match goal with H: context[w_mul_c] |- _ =>
   generalize H; clear H
 end.
 rewrite _w0_is_0.
 unfold w_mul_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_mul_c.
 simpl; rewrite _w0_is_0, Zmult_0_l, Zplus_0_l.
 intros H2; rewrite H2; simpl.
 rewrite Z_mod_same; auto with zarith.
 generalize (high_zero (w_mul_c w2 w3)).
 unfold w_mul_c; generalize (ZnZ.spec_mul_c w2 w3);
  case (ZnZ.mul_c w2 w3); simpl.
 intros H3 _  _; rewrite <- H3; autorewrite with w_rewrite; auto.
(*  rewrite Zmod_small; auto with zarith. *)
 intros w4 w5.
 change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0.
 change (w_to_Z w4) with [|w4|].
 change (w_to_Z w5) with [|w5|].
 simpl.
 intros H2 H3 H4.
 assert (E1: [|w4|] = 0).
 apply H3.
 apply Z.lt_trans with (1 := H4).
 case (ZnZ.spec_to_Z b); auto with zarith.
 generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l;
   clear H4 H2; intros H4 H2.
 rewrite <- H2; rewrite Zmod_small. auto with zarith.
 case (ZnZ.spec_to_Z w5); auto with zarith.
 intros H2.
 match goal with |- context[split ?x] =>
 generalize (split_correct x);
  case (split x); auto with zarith
 end.
 assert (F1: [[w_mul_c w2 w3]] < [|b|] * [|b|]).
 unfold w_to_Z, w_mul_c, ww_to_Z,w_digits;
   rewrite ZnZ.spec_mul_c.
 apply Zmult_lt_compat.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 case (ZnZ.spec_to_Z w3); auto with zarith.
 intros w4 w5; rewrite ww_lsl_n_spec. 2: auto with zarith.
 intros H3.
 unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] =>
   generalize (ZnZ.spec_div21 y z t);
   case (ZnZ.div21 y z t)
 end.
 rewrite b2n_spec; case (n_spec).
 intros H4 H5 w6 w7 H6.
 case H6. auto with zarith.
 case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7.
 match type of H3 with ?X = ?Y =>
    absurd (Y < X)
 end.
 apply Zle_not_lt; rewrite H3. auto with zarith.
 simpl ww_to_Z.
 match goal with |- ?X < ?Y + _ =>
    apply Z.lt_le_trans with Y; auto with zarith
 end.
 apply Z.lt_trans with (2 ^ [|n|] * ([|b|] * [|b|]));
   auto with zarith.
 apply Zmult_lt_compat_l; auto with zarith.
 rewrite Zmult_assoc.
 apply Zmult_lt_compat2; auto with zarith.
 case (ZnZ.spec_to_Z b); auto with zarith.
 case (ZnZ.spec_to_Z w5); unfold w_to_Z;auto with zarith.
 clear H6; intros H7 H8.
 rewrite w_lsr_n_spec by auto with zarith.
 rewrite <- (Z_div_mult ([|w2|] * [|w3|]) (2 ^ [|n|]))
  by auto with zarith; rewrite Zmult_comm.
 rewrite <- ZnZ.spec_mul_c.
 unfold w_mul_c in H3; unfold ww_to_Z in H3;simpl in H3.
 unfold w_digits,w_to_Z in H3. rewrite <- H3; simpl.
 rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x));
   rewrite Zmult_assoc; rewrite  BigNumPrelude.Z_div_plus_l by auto with zarith.
 rewrite Zplus_mod.
 rewrite Z_mod_mult.
 rewrite Zplus_0_l.
 rewrite Zmod_mod.
 rewrite Zmod_small. auto with zarith.
 split. auto with zarith.
 apply Zdiv_lt_upper_bound. auto with zarith.
 rewrite Zmult_comm; auto with zarith.
 Qed.

 Let _square_mod x :=
  let x2 := w_square_c x in
  match ww_compare x2 wwb with
  | Lt => snd (split x2)
  | Eq => w0
  | Gt =>
    let x2_2n := ww_lsl_n x2 in
    let (h,l) := split x2_2n in
    let (q,r) := w_div21 h l b2n in
    w_lsr_n r
  end.

 Lemma _square_mod_spec: forall w t, [|w|] = t mod [|b|] ->
    [|_square_mod w|] = ([|w|] * [|w|]) mod [|b|].
 intros w2 t2 H; unfold _square_mod, wwb.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t2 [|b|]); auto with zarith.
 match goal with |- context[ww_compare ?x ?y] =>
   change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y)
 end.
 rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare
    ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare); case Z.compare_spec;
   intros H2;
 match goal with H: context[w_square_c] |- _ =>
   generalize H; clear H
 end; autorewrite with w_rewrite.
 rewrite _w0_is_0.
 unfold w_square_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_square_c.
 intros H2;rewrite H2; simpl.
 rewrite _w0_is_0; simpl.
 rewrite Z_mod_same; auto with zarith.
 generalize (high_zero (w_square_c w2)).
 unfold w_square_c; generalize (ZnZ.spec_square_c w2);
  case (ZnZ.square_c w2); simpl; auto with zarith.
 intros H3 _  _; rewrite <- H3; autorewrite with w_rewrite; auto.
 intros w4 w5.
 change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0; simpl.
 change (w_to_Z w4) with [|w4|].
 change (w_to_Z w5) with [|w5|].
 intros H2 H3 H4.
 assert (E1: [|w4|] = 0).
 apply H3.
 apply Z.lt_trans with (1 := H4).
 case (ZnZ.spec_to_Z b); auto with zarith.
 generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l;
   clear H4 H2; intros H4 H2.
 rewrite <- H2; rewrite Zmod_small. auto with zarith.
 case (ZnZ.spec_to_Z w5); auto with zarith.
 intros H2.
 match goal with |- context[split ?x] =>
 generalize (split_correct x);
  case (split x); auto with zarith
 end.
 assert (F1: [[w_square_c w2]] < [|b|] * [|b|]).
 unfold w_square_c, ww_to_Z, w_digits, w_to_Z.
 rewrite ZnZ.spec_square_c.
 apply Zmult_lt_compat.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 intros w4 w5; rewrite ww_lsl_n_spec by auto with zarith.
 intros H3.
 unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] =>
   generalize (ZnZ.spec_div21 y z t);
   case (ZnZ.div21 y z t)
 end.
 rewrite b2n_spec; case (n_spec); auto.
 intros H4 H5 w6 w7 H6.
 case H6. auto with zarith.
 case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7.
 match type of H3 with ?X = ?Y =>
    absurd (Y < X)
 end.
 apply Zle_not_lt; rewrite H3; auto with zarith.
 simpl ww_to_Z.
 match goal with |- ?X < ?Y + _ =>
    apply Z.lt_le_trans with Y; auto with zarith
 end.
 apply Z.lt_trans with (2 ^ [|n|] * ([|b|] * [|b|])).
 apply Zmult_lt_compat_l; auto with zarith.
 rewrite Zmult_assoc.
 apply Zmult_lt_compat2. auto with zarith.
 case (ZnZ.spec_to_Z b); auto with zarith.
 unfold w_to_Z,w_digits;case (ZnZ.spec_to_Z w5). auto with zarith.
 clear H6; intros H7 H8.
 rewrite w_lsr_n_spec by auto with zarith.
 rewrite <- (Z_div_mult ([|w2|] * [|w2|]) (2 ^ [|n|]))
  by auto with zarith; rewrite Zmult_comm.
 rewrite <- ZnZ.spec_square_c.
 unfold w_square_c, ww_to_Z in H3;  unfold w_digits,w_to_Z in H3.
 rewrite <- H3; simpl.
 rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x));
   rewrite Zmult_assoc; rewrite BigNumPrelude.Z_div_plus_l by auto with zarith.
 rewrite Zplus_mod.
 rewrite Z_mod_mult.
 rewrite Zplus_0_l.
 rewrite Zmod_mod.
 rewrite Zmod_small. auto with zarith.
 split. auto with zarith.
 apply Zdiv_lt_upper_bound. auto with zarith.
 rewrite Zmult_comm; auto with zarith.
 Qed.

 Let _power_mod :=
   fix pow_mod (x:w) (p:positive) {struct p} : w :=
     match p with
     | xH => x
     | xO p' =>
       let pow := pow_mod x p' in
       _square_mod pow
     | xI p' =>
       let pow := pow_mod x p' in
       _mul_mod (_square_mod pow) x
     end.

 Lemma _power_mod_spec: forall w t p, [|w|] = t mod [|b|] ->
   [|_power_mod w p|] = (Zpower_pos [|w|] p) mod [|b|].
 intros w2 t p; elim p; simpl; auto with zarith.
 intros p' Rec H.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t [|b|]); auto with zarith.
 replace (xI p') with (p' + p' + 1)%positive.
 repeat rewrite Zpower_pos_is_exp; auto with zarith.
 pose (t1 := [|_power_mod w2 p'|]).
 rewrite _mul_mod_spec with (t1 := t1 * t1)
                            (t2 := t); auto with zarith.
 rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith.
 rewrite Rec; auto with zarith.
 assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp).
 intros p1; unfold Zpower_pos; simpl; ring.
 rewrite <- Zmult_mod; auto with zarith.
 rewrite Zmult_mod; auto with zarith.
 rewrite Zmod_mod; auto with zarith.
 rewrite <- Zmult_mod; auto with zarith.
 simpl; unfold t1; apply _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith.
 rewrite xI_succ_xO; rewrite <- Pplus_diag.
 rewrite Pplus_one_succ_r; auto.
 intros p' Rec H.
 replace (xO p') with (p' + p')%positive.
 repeat rewrite Zpower_pos_is_exp; auto with zarith.
 rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith.
 rewrite Rec; auto with zarith.
 rewrite <- Zmult_mod; auto with zarith.
 rewrite <- Pplus_diag; auto.
 intros H.
 assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp).
 intros p1; unfold Zpower_pos; simpl; ring.
 rewrite Zmod_small; auto with zarith.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t [|b|]); auto with zarith.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 Qed.

 Definition make_mod_op :=
   mk_mod_op
     _succ_mod _add_mod
     _pred_mod _sub_mod
     _mul_mod _square_mod _power_mod.

  Definition make_mod_spec: mod_spec make_mod_op.
  apply mk_mod_spec.
  exact _succ_mod_spec.
  exact _add_mod_spec.
  exact _pred_mod_spec.
  exact _sub_mod_spec.
  exact _mul_mod_spec.
  exact _square_mod_spec.
  exact _power_mod_spec.
  Defined.

(*********** Mersenne special **********)

 Variable p: positive.
 Variable zp: w.

 Hypothesis zp_b: [|zp|] = Zpos p.
 Hypothesis p_lt_w_digits: Zpos p <= Zpos w_digits.

 Let p1 := Pminus (xO w_digits) p.

 Theorem p_p1: Zpos p + Zpos p1 = Zpos (xO w_digits).
 unfold p1.
 rewrite Zpos_minus.
 rewrite Zmax_right.
 auto with zarith.
 rewrite Zpos_xO.
 assert (0 < Zpos w_digits); auto with zarith.
 Qed.

 Let zp1 := ww_sub ww_zdigits (WW w0 zp).

 Let spec_add2: forall x y,
  [[w_add2 x y]] = [|x|] + [|y|].
  unfold w_add2.
  intros xh xl; generalize (ZnZ.spec_add_c xh xl).
  unfold w_add_c; case ZnZ.add_c; unfold interp_carry; simpl ww_to_Z.
    intros w2 Hw2; simpl; unfold w_to_Z; rewrite Hw2.
  unfold w0; rewrite ZnZ.spec_0; simpl; auto with zarith.
  intros w2; rewrite Zmult_1_l; simpl.
  unfold w_to_Z, w1; rewrite ZnZ.spec_1; auto with zarith.
  rewrite Zmult_1_l; auto.
 Qed.

 Let spec_ww_digits:
  [[ww_zdigits]] = Zpos (xO w_digits).
 Proof.
 unfold w_to_Z, ww_zdigits.
 rewrite spec_add2.
 unfold w_to_Z, w_zdigits, w_digits.
 rewrite ZnZ.spec_zdigits; auto.
 rewrite Zpos_xO; auto with zarith.
 Qed.

 Let spec_ww_to_Z := (spec_ww_to_Z _ _ ZnZ.spec_to_Z).
 Let spec_ww_compare := spec_ww_compare _ _ _ _ ZnZ.spec_0
      ZnZ.spec_to_Z ZnZ.spec_compare.
 Let spec_ww_sub :=
         spec_ww_sub w0 zp wWW zp1 w_opp_c w_opp_carry
              w_sub_c w_opp w_sub w_sub_carry w_digits w_to_Z
             ZnZ.spec_0
             ZnZ.spec_to_Z
             ZnZ.spec_WW
             ZnZ.spec_opp_c
             ZnZ.spec_opp
             ZnZ.spec_opp_carry
             ZnZ.spec_sub_c
             ZnZ.spec_sub
             ZnZ.spec_sub_carry.

 Theorem zp1_b: [[zp1]] = Zpos p1.
 change ([[DoubleSub.ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub
            w_sub_carry ww_zdigits (WW w0 zp)]] =
          Zpos p1).
 rewrite spec_ww_sub.
 rewrite spec_ww_digits; simpl ww_to_Z.
 change (w_to_Z w0) with [|w0|].
 unfold w0; rewrite ZnZ.spec_0; autorewrite with rm10.
 change (w_to_Z zp) with [|zp|].
 rewrite zp_b.
 rewrite Zmod_small.
 rewrite <- p_p1; ring.
 unfold ww_digits; split.
 rewrite <- p_p1.
 assert (0 < Zpos p1); auto with zarith.
 apply Z.le_lt_trans with (Zpos (xO w_digits)).
 assert (0 < Zpos p); auto with zarith.
 unfold base; apply Zpower2_lt_lin; auto with zarith.
 Qed.

 Hypothesis p_b: [|b|] = 2 ^ (Zpos p) - 1.

 Let w_pos_mod := ZnZ.pos_mod.

 Let add_mul_div :=
   DoubleLift.ww_add_mul_div w0 wWW wW0 w0W
              ww_compare w_add_mul_div
              ww_sub w_zdigits low.

 Let _mmul_mod x y :=
  let xy := w_mul_c x y in
  match xy with
    W0 => w0
  | WW xh xl =>
      let xl1 := w_pos_mod zp xl in
        match add_mul_div zp1 W0 xy with
          W0 => match w_compare xl1 b with
                | Lt => xl1
                | Eq => w0
                | Gt => w1
                end
        | WW _ xl2 => _add_mod xl1 xl2
        end
  end.

 Hint Unfold w_digits : core.

 Lemma WW_0: forall x y, [[WW x y]] = 0 -> [|x|] = 0 /\ [|y|] =0.
 intros x y; simpl; case (ZnZ.spec_to_Z x); intros H1 H2;
   case (ZnZ.spec_to_Z y); intros H3 H4 H5.
 case Zle_lt_or_eq with (1 := H1); clear H1; intros H1.
 absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]).
 unfold w_to_Z, w_digits in H5;auto with zarith.
 match goal with |- _ < ?X + _ =>
  apply Z.lt_le_trans with X; auto with zarith
 end.
 case Zle_lt_or_eq with (1 := H3); clear H3; intros H3. 2: auto with zarith.
 absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]).
 unfold w_to_Z, w_digits in H5; auto with zarith.
 rewrite <- H1; rewrite Zmult_0_l; auto with zarith.
 Qed.

 Theorem WW0_is_0: [[W0]] = 0.
 simpl; auto.
 Qed.
  Hint Rewrite WW0_is_0: w_rewrite.

 Theorem mmul_aux0: Zpos (xO w_digits) - Zpos p1 = Zpos p.
 unfold w_digits.
 apply trans_equal with (Zpos p + Zpos p1 - Zpos p1).
 rewrite p_p1; auto with zarith.
 auto with zarith.
 Qed.

 Theorem mmul_aux1: 2 ^ Zpos w_digits =
     2 ^ (Zpos w_digits - Zpos p) * 2 ^ Zpos p.
 rewrite <- Zpower_exp; auto with zarith.
 eq_tac; auto with zarith.
 Qed.

 Theorem mmul_aux2:forall x,
   x mod (2 ^ Zpos p - 1) =
    ((x / 2 ^ Zpos p) + (x mod 2 ^ Zpos p)) mod (2 ^ Zpos p - 1).
 intros x; pattern x at 1; rewrite Z_div_mod_eq_full with (b := 2 ^ Zpos p).
 match goal with |- (?X * ?Y + ?Z) mod (?X - 1) = ?T =>
  replace (X * Y + Z) with (Y * (X - 1) + (Y + Z)); try ring
 end.
 rewrite Zplus_mod; auto with zarith.
 rewrite Z_mod_mult; auto with zarith.
 rewrite Zplus_0_l.
 rewrite Zmod_mod; auto with zarith.
 Qed.

 Theorem mmul_aux3:forall xh xl,
   [[WW xh xl]] mod (2 ^ Zpos p) = [|xl|] mod (2 ^ Zpos p).
 intros xh xl; simpl ww_to_Z; unfold base.
 rewrite Zplus_mod; auto with zarith.
 generalize mmul_aux1; unfold w_digits; intros tmp; rewrite tmp;
   clear tmp.
 rewrite Zmult_assoc.
 rewrite Z_mod_mult; auto with zarith.
 rewrite Zplus_0_l; apply Zmod_mod; auto with zarith.
 Qed.

 Let spec_low: forall x,
  [|low x|] = [[x]] mod base w_digits.
  intros x; case x; simpl low; auto with zarith.
  intros xh xl; simpl.
  rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith.
  rewrite Zmod_small; auto with zarith.
  case (ZnZ.spec_to_Z xl); auto with zarith.
  unfold base; auto with zarith.
 Qed.

 Theorem mmul_aux4:forall x,
  [[x]] < [|b|] * 2 ^  Zpos p ->
     match add_mul_div zp1 W0 x with
          W0 => 0
        | WW _ xl2 => [|xl2|]
     end = [[x]] / 2 ^ Zpos p.
 intros x Hx.
 assert (Hp: [[zp1]] <= Zpos (xO w_digits)).
   rewrite zp1_b; rewrite <- p_p1.
   assert (0 <= Zpos p); auto with zarith.
 generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W
    ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z
    ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z
    ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW
    spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub
    ZnZ.spec_zdigits spec_low W0 x zp1 Hp).
  unfold add_mul_div;
    case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite.
 rewrite Zmult_0_l; rewrite Zplus_0_l.
 rewrite zp1_b.
 generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp.
 rewrite Zmod_small. auto with zarith.
 split.
 apply Z_div_pos. auto with zarith.
 case (spec_ww_to_Z x); auto with zarith.
 unfold base.
 apply Zdiv_lt_upper_bound. auto with zarith.
 rewrite <- Zpower_exp by auto with zarith.
 apply Z.lt_le_trans with (base (ww_digits (ZnZ.digits w_op))).
   case (spec_ww_to_Z x); auto with zarith.
 unfold base; apply Zpower_le_monotone. auto with zarith.
 split. auto with zarith.
 assert (0 < Zpos p); auto with zarith.
 intros w2 w3; rewrite Zmult_0_l; rewrite Zplus_0_l.
 rewrite zp1_b.
 generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp;
  clear tmp.
 simpl ww_to_Z; rewrite Zmod_small.
 intros H1;
   generalize (high_zero (WW w2 w3)); unfold w_digits;intros tmp;
   simpl fst in tmp; simpl ww_to_Z in tmp.
   unfold w_to_Z in *.
   rewrite tmp in H1. auto with zarith. clear tmp.
 simpl ww_to_Z; rewrite H1; apply Zdiv_lt_upper_bound. auto with zarith.
 unfold base; rewrite <- Zpower_exp by auto with zarith.
 apply Z.lt_le_trans with (1 := Hx).
 apply Z.le_trans with (2 ^ Zpos p * 2 ^ Zpos p).
 rewrite p_b; apply Zmult_le_compat_r; auto with zarith.
 rewrite <- Zpower_exp by auto with zarith.
 apply Zpower_le_monotone; auto with zarith.
 split.
 apply Z_div_pos. auto with zarith.
 case (spec_ww_to_Z  x); auto with zarith.
 unfold base.
 apply Zdiv_lt_upper_bound. auto with zarith.
 rewrite <- Zpower_exp by auto with zarith.
 apply Z.lt_le_trans with (base (ww_digits (ZnZ.digits w_op))).
   case (spec_ww_to_Z x); auto with zarith.
 unfold base; apply Zpower_le_monotone. auto with zarith.
 split. auto with zarith.
 assert (0 < Zpos p); auto with zarith.
 Qed.

 Theorem mmul_aux5:forall xh xl,
      [[WW xh xl]] < [|b|] * 2 ^  Zpos p ->
      let xl1 := w_pos_mod zp xl in
      let r :=
        match add_mul_div zp1 W0 (WW xh xl) with
          W0 => match w_compare xl1 b with
                | Lt => xl1
                | Eq => w0
                | Gt => w1
                end
        | WW _ xl2 => _add_mod xl1 xl2
        end  in
        [|r|] = [[WW xh xl]] mod [|b|].
 intros xh xl Hx xl1 r; unfold r; clear r.
 generalize (mmul_aux4 _ Hx).
 simpl ww_to_Z; rewrite p_b.
 rewrite mmul_aux2.
 assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith.
   rewrite zp1_b; rewrite <- p_p1; auto with zarith.
   assert (0 <= Zpos p); auto with zarith.
 generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W
    ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z
    ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z
    ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW
    spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub
    ZnZ.spec_zdigits spec_low W0 (WW xh xl) zp1 Hp).
  unfold add_mul_div;
    case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto.
 rewrite Zmult_0_l; rewrite Zplus_0_l.
 rewrite zp1_b.
 generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp.
 intros H1 H2.
 rewrite <- H2.
 rewrite Zplus_0_l.
 generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp;
   auto with zarith.
 unfold xl1; unfold w_pos_mod.
  rewrite <- p_b; rewrite <- zp_b.
  rewrite <- ZnZ.spec_pos_mod; auto with zarith.
 unfold w_compare; rewrite ZnZ.spec_compare;
   case Z.compare_spec; intros Hc;
 match goal with H: context[b] |- _ =>
   generalize H; clear H
 end; try rewrite _w0_is_0.
 intros H3; rewrite H3.
 rewrite Z_mod_same; auto with zarith.
 intros H3; rewrite Zmod_small; auto with zarith.
 case (ZnZ.spec_to_Z (ZnZ.pos_mod zp xl)); unfold w_to_Z; auto with zarith.
 rewrite p_b; rewrite ZnZ.spec_pos_mod; auto with zarith.
 intros H3; assert (HH: [|xl|] mod 2 ^ Zpos p = 2 ^ Zpos p).
 apply Zle_antisym; auto with zarith.
 case (Z_mod_lt ([|xl|]) (2 ^ Zpos p)); auto with zarith.
 rewrite zp_b in H3; auto with zarith.
 rewrite zp_b; rewrite HH.
 rewrite <- Zmod_minus_one; auto with zarith.
 rewrite _w1_is_1; rewrite Zmod_small; auto with zarith.
 rewrite Zmult_0_l; rewrite Zplus_0_l.
 rewrite zp1_b.
 generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp.
 intros w2 w3 H1 H2; rewrite <- H2.
 generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp;
   auto with zarith.
 rewrite <- p_b; rewrite <- zp_b.
 rewrite <- ZnZ.spec_pos_mod; auto with zarith.
 unfold xl1; unfold w_pos_mod.
 rewrite Zplus_comm.
 apply _add_mod_correct; auto with zarith.
 assert (tmp: forall x, 2 * x = x + x); auto with zarith;
   rewrite tmp; apply Zplus_le_lt_compat; clear tmp; auto with zarith.
 rewrite ZnZ.spec_pos_mod; auto with zarith.
 rewrite p_b; case (Z_mod_lt [|xl|] (2 ^ Zpos p)); auto with zarith.
 rewrite zp_b; auto with zarith.
 rewrite H2; apply Zdiv_lt_upper_bound; auto with zarith.
 Qed.

 Lemma _mmul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] ->
   [|_mmul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|].
 intros w2 w3 t1 t2; unfold _mmul_mod, w_mul_c; intros H H1.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t1 [|b|]); auto with zarith.
 assert (F': [|w3|] < [|b|]).
 case (Z_mod_lt t2 [|b|]); auto with zarith.
 match goal with |- context[ZnZ.mul_c ?x ?y] =>
   generalize (ZnZ.spec_mul_c x y); unfold interp_carry;
   case (ZnZ.mul_c x y); autorewrite with w_rewrite
 end; auto with zarith.
 simpl; intros H2; rewrite <- H2; rewrite Zmod_small;
  auto with zarith.
 intros w4 w5 H2.
 rewrite mmul_aux5; auto with zarith.
 rewrite <- H2; auto.
 unfold ww_to_Z,w_digits,w_to_Z; rewrite H2.
 apply Zmult_lt_compat; auto with zarith.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 case (ZnZ.spec_to_Z w3); auto with zarith.
 Qed.

 Let _msquare_mod x :=
  let xy := w_square_c x in
  match xy with
    W0 => w0
  | WW xh xl =>
      let xl1 := w_pos_mod zp xl in
        match add_mul_div zp1 W0 xy with
          W0 =>  match w_compare xl1 b with
                | Lt => xl1
                | Eq => w0
                | Gt => w1
                end
        | WW _ xl2 => _add_mod xl1 xl2
        end
  end.

 Lemma _msquare_mod_spec: forall w1 t1, [|w1|] = t1 mod [|b|] ->
   [|_msquare_mod w1|] = ([|w1|] * [|w1|]) mod [|b|].
 intros w2 t2; unfold _msquare_mod, w_square_c; intros H.
 assert (F: [|w2|] < [|b|]).
 case (Z_mod_lt t2 [|b|]); auto with zarith.
 match goal with |- context[ZnZ.square_c ?x] =>
   generalize (ZnZ.spec_square_c x); unfold interp_carry;
   case (ZnZ.square_c x); autorewrite with w_rewrite
 end; auto with zarith.
 simpl; intros H2; rewrite <- H2; rewrite Zmod_small;
  auto with zarith.
 intros w4 w5 H2.
 rewrite mmul_aux5; auto with zarith.
 unfold ww_to_Z, w_to_Z ,w_digits; rewrite <- H2; auto.
 unfold ww_to_Z,w_to_Z ,w_digits; rewrite H2.
 apply Zmult_lt_compat; auto with zarith.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 case (ZnZ.spec_to_Z w2); auto with zarith.
 Qed.

 Definition mmake_mod_op :=
   mk_mod_op
     _succ_mod _add_mod
     _pred_mod _sub_mod
     _mmul_mod _msquare_mod _power_mod.

 Definition mmake_mod_spec: mod_spec mmake_mod_op.
  apply mk_mod_spec.
  exact _succ_mod_spec.
  exact _add_mod_spec.
  exact _pred_mod_spec.
  exact _sub_mod_spec.
  exact _mmul_mod_spec.
  exact _msquare_mod_spec.
  exact _power_mod_spec.
  Defined.

End Mod_op.

author: thery

repo: coqprime

save_path: github-repos/coq/thery-coqprime


text:
Require Export Coq.Program.Tactics.
Require Export Coq.Setoids.Setoid.
Require Export Coq.Classes.Morphisms.
Require Export Coq.Arith.Arith_base.
Require Export Coq.Relations.Relations.
Require Export Coq.Lists.List.

Import EqNotations.
Import ListNotations.

(***
 *** Ordered Types = Types with a PreOrder
 ***)

(* NOTE: The idea with this approach is that each type uniquely determines its
ordered type, but we keep the types separate from the ordered types to make
type inference work properly... *)

Class OType (A:Type) : Type :=
  {
    oleq : relation A;
    oPreOrder :> PreOrder oleq
  }.

Instance OType_Reflexive A `{OType A} : Reflexive oleq.
Proof. typeclasses eauto. Qed.

Instance OType_Transitive A `{OType A} : Transitive oleq.
Proof. typeclasses eauto. Qed.

(* The equivalence relation for an OrderedType *)
Definition oeq {A} `{OType A} : relation A :=
  fun x y => oleq x y /\ oleq y x.

Instance oeq_Equivalence A `{OType A} : Equivalence oeq.
Proof.
  constructor; intro; intros.
  { split; reflexivity. }
  { destruct H0; split; assumption. }
  { destruct H0; destruct H1; split; transitivity y; assumption. }
Qed.

Notation "x <o= y" :=
  (oleq x y) (no associativity, at level 70).
Notation "x =o= y" :=
  (oeq x y) (no associativity, at level 70).

(* FIXME: replace "oleq" below with "<o=" notation *)

(* FIXME: figure out what versions of this we need for rewriting! *)
Instance Proper_oleq_oleq A `{OType A}
  : Proper (oleq --> oleq ==> Basics.impl) (@oleq A _).
Proof.
  intros a1 a2 Ra b1 b2 Rb Rab.
  transitivity a1; [ assumption | ]. transitivity b1; assumption.
Qed.

Instance Subrelation_oeq_oleq A `{OType A} :
  subrelation (@oeq A _) oleq.
Proof.
  intros a1 a2 Ra; destruct Ra; assumption.
Qed.

Instance Proper_oeq_oleq A `{OType A} :
  Proper (oeq ==> oeq ==> iff) (@oleq A _).
Proof.
  intros x1 x2 Rx y1 y2 Ry; destruct Rx; destruct Ry; split; intro Rxy.
  transitivity x1; [ assumption | ]; transitivity y1; assumption.
  transitivity x2; [ assumption | ]; transitivity y2; assumption.
Qed.

Instance Proper_oeq A `{OType A} :
  Proper (oeq ==> oeq ==> iff) (@oeq A _).
Proof.
  intros x1 x2 Rx y1 y2 Ry. rewrite Rx. rewrite Ry. reflexivity.
Qed.

Instance Proper_oeq_partial A `{OType A} a :
  Proper (oeq ==> Basics.flip Basics.impl) (@oeq A _ a).
Proof.
  intros x1 x2 Rx. rewrite Rx. reflexivity.
Qed.

(***
 *** Commonly-Used Ordered Types
 ***)

(* The ordered type of propositions *)
Instance OTProp : OType Prop :=
  {| oleq := Basics.impl |}.
Proof. repeat constructor; typeclasses eauto. Defined.

(* Proofs are always related (i.e., this is the proof irrelevance type) *)
Instance OTproof (P:Prop) : OType P :=
  {| oleq := fun _ _ => True |}.
Proof.
  repeat constructor.
Defined.

(* The discrete ordered type, where things are only related to themselves; we
make this a definition, not an instance, so that it can be instantiated for
particular types. *)
Definition OTdiscrete A : OType A := {| oleq := eq |}.

(* The only ordered type over unit is the discrete one *)
Instance OTunit : OType unit := OTdiscrete unit.

(* The ordered type that flips the ordering of an underlying OType; this becomes
a type itself in Coq *)
Inductive Flip A : Type := flip (a:A).
Arguments flip {A} a.

Definition unflip {A} (f:Flip A) : A := let (x) := f in x.

Instance OTFlip A (R:OType A) : OType (Flip A) :=
  {| oleq := fun x y => unflip y <o= unflip x |}.
Proof.
  repeat constructor; intro; intros.
  - destruct x; compute; reflexivity.
  - destruct x; destruct y; destruct z; compute; transitivity a0; assumption.
Defined.

(* The discrete relation on Booleans *)
Instance OTbool : OType bool := OTdiscrete bool.

(* The pointwise relation on pairs *)
Instance OTpair A B `(OType A) `(OType B) : OType (A*B) :=
  {| oleq := fun p1 p2 => oleq (fst p1) (fst p2) /\ oleq (snd p1) (snd p2) |}.
Proof.
  repeat constructor.
  - destruct x. reflexivity.
  - destruct x. reflexivity.
  - destruct x; destruct y; destruct z; destruct H1; destruct H2;
      transitivity a0; assumption.
  - destruct x; destruct y; destruct z; destruct H1; destruct H2;
      transitivity b0; assumption.
Defined.

(* The sort-of pointwise relation on sum types *)
Inductive sumR {A B} (RA:OType A) (RB:OType B) : A+B -> A+B -> Prop :=
| sumR_inl a1 a2 : oleq a1 a2 -> sumR RA RB (inl a1) (inl a2)
| sumR_inr b1 b2 : oleq b1 b2 -> sumR RA RB (inr b1) (inr b2).

Instance OTsum A B (RA:OType A) (RB:OType B) : OType (A+B) :=
  {| oleq := sumR RA RB |}.
Proof.
  repeat constructor; intro; intros.
  { destruct x; constructor; reflexivity. }
  { destruct H; inversion H0.
    - constructor; transitivity a2; assumption.
    - constructor; transitivity b2; assumption. }
Defined.

(* NOTE: the following definition requires everything above to be polymorphic *)
(* NOTE: The definition we choose for OTType is actually deep: instead of
requiring ot_Type A = ot_Type B, we could just require a coercion function from
ot_Type A to ot_Type B, which would yield something more like HoTT... though
maybe it wouldn't work unless we assumed the HoTT axiom? As it is, we might need
UIP to hold if we want to use the definition given here... *)
(*
Program Definition OTType : OType :=
  {|
    ot_Type := OType;
    oleq := (fun A B =>
               exists (e:ot_Type A = ot_Type B),
                 forall (x y:A),
                   oleq A x y ->
                   oleq B (rew [fun A => A] e in x)
                        (rew [fun A => A] e in y));
  |}.
*)

(***
 *** Proper Instances for Simple Ordered Types
 ***)

Instance Proper_pair A B `{OType A} `{OType B} :
  Proper (oleq ==> oleq ==> oleq) (pair : A -> B -> A*B).
Proof.
  repeat intro; split; assumption.
Qed.

Instance Proper_pair_equiv A B `{OType A} `{OType B} :
  Proper (oeq ==> oeq ==> oeq) (pair : A -> B -> A*B).
Proof.
  intros a1 a2 Ra b1 b2 Rb; destruct Ra; destruct Rb; split; split; assumption.
Qed.

Instance Proper_fst A B `{OType A} `{OType B} :
  Proper (oleq ==> oleq) (fst : A*B -> A).
Proof.
  intros p1 p2 Rp; destruct Rp; assumption.
Qed.

Instance Proper_fst_equiv A B `{OType A} `{OType B} :
  Proper (oeq ==> oeq) (fst : A*B -> A).
Proof.
  intros p1 p2 Rp. destruct Rp.
  split; eapply Proper_fst; assumption.
Qed.

Instance Proper_snd A B `{OType A} `{OType B} :
  Proper (oleq ==> oleq) (snd : A*B -> B).
Proof.
  intros p1 p2 Rp; destruct Rp; assumption.
Qed.

Instance Proper_snd_equiv A B `{OType A} `{OType B} :
  Proper (oeq ==> oeq) (snd : A*B -> B).
Proof.
  intros p1 p2 Rp. destruct Rp.
  split; eapply Proper_snd; assumption.
Qed.

(***
 *** The Ordered Type for Functions
 ***)

(* The type of continuous, i.e. Proper, functions between ordered types *)
Record OFun A B {RA:OType A} {RB:OType B} :=
  {
    ofun_app : A -> B;
    ofun_Proper : Proper (oleq ==> oleq) ofun_app
  }.

Arguments ofun_app {_ _ _ _} _ _.
Arguments ofun_Proper [_ _ _ _] _ _ _ _.

Notation "A '-o>' B" :=
  (OFun A B) (right associativity, at level 99).
Notation "x @o@ y" :=
  (ofun_app x y) (left associativity, at level 20).

(* The non-dependent function ordered type *)
Instance OTarrow A B `{OType A} `{OType B} : OType (A -o> B) :=
  {| oleq :=
       fun f g =>
         forall a1 a2, oleq a1 a2 -> oleq (ofun_app f a1) (ofun_app g a2) |}.
Proof.
  repeat constructor; intro; intros.
  { apply ofun_Proper; assumption. }
  { transitivity (ofun_app y a1).
    - apply H1; reflexivity.
    - apply H2; assumption. }
Defined.

(* FIXME: could also do a forall type, but need the second type argument, B, to
itself be proper, i.e., to be an element of OTarrow A OType. *)

(* ofun_app is always Proper *)
Instance Proper_ofun_app A B `{OType A} `{OType B} :
  Proper (oleq ==> oleq ==> oleq) (@ofun_app A B _ _).
Proof.
  intros f1 f2 Rf a1 a2 Ra. apply Rf; assumption.
Qed.

(* ofun_app is always Proper w.r.t. oeq *)
Instance Proper_ofun_app_equiv A B `{OType A} `{OType B} :
  Proper (oeq ==> oeq ==> oeq) (@ofun_app A B _ _).
Proof.
  intros f1 f2 Rf a1 a2 Ra; destruct Rf; destruct Ra.
  split; apply Proper_ofun_app; assumption.
Qed.

Instance Proper_ofun_app_partial A B `{OType A} `{OType B} f :
  Proper (oleq ==> oleq) (ofun_app (A:=A) (B:=B) f).
Proof.
  apply ofun_Proper.
Qed.

Instance Proper_ofun_app_partial_equiv A B `{OType A} `{OType B} f :
  Proper (oeq ==> oeq) (@ofun_app A B _ _ f).
Proof.
  intros a1 a2 Ra; destruct Ra; split; apply ofun_Proper; assumption.
Qed.

(***
 *** Some Useful OFuns
 ***)

(* The identity ofun *)
Definition id_ofun {A} `{OType A} : A -o> A :=
  {| ofun_app := fun x => x; ofun_Proper := fun x1 x2 Rx => Rx |}.

(* The identity ofun *)
Program Definition compose_ofun {A B C}
        `{OType A} `{OType B} `{OType C}
        (f:A -o> B) (g:B -o> C) : A -o> C :=
  {| ofun_app := fun x => ofun_app g (ofun_app f x);
     ofun_Proper := _ |}.
Next Obligation.
  intros x1 x2 Rx. apply ofun_Proper. apply ofun_Proper. assumption.
Qed.

Instance Proper_compose_ofun A B C
         `{OType A} `{OType B} `{OType C} :
  Proper (oleq ==> oleq ==> oleq) (@compose_ofun A B C _ _ _).
  intros f1 f2 Rf g1 g2 Rg a1 a2 Ra.
  apply Rg. apply Rf. assumption.
Qed.

Instance Proper_compose_ofun_equiv A B C
         `{OType A} `{OType B} `{OType C} :
  Proper (oeq ==> oeq ==> oeq) (@compose_ofun A B C _ _ _).
Proof.
  intros f1 f2 Rf g1 g2 Rg.
  split; intros a1 a2 Ra; simpl; apply Rg; apply Rf; apply Ra.
Qed.

(* Category theory laws for OFuns *)
Lemma id_compose_ofun A B `{OType A} `{OType B} (f: A -o> B) :
  oeq (compose_ofun id_ofun f) f.
  split; intros a1 a2 Ra; simpl; apply ofun_Proper; assumption.
Qed.
Lemma compose_id_ofun A B `{OType A} `{OType B} (f: A -o> B) :
  oeq (compose_ofun f id_ofun) f.
  split; intros a1 a2 Ra; simpl; apply ofun_Proper; assumption.
Qed.
Lemma compose_compose_ofun A B C D
      `{OType A} `{OType B} `{OType C} `{OType D}
      (f: A -o> B) (g: B -o> C) (h: C -o> D) :
  oeq (compose_ofun f (compose_ofun g h)) (compose_ofun (compose_ofun f g) h).
  split; intros a1 a2 Ra; simpl; repeat apply ofun_Proper; assumption.
Qed.

(* The constant ofun *)
Program Definition const_ofun {A B} `{OType A} `{OType B} b : A -o> B :=
  {| ofun_app := fun _ => b; ofun_Proper := fun _ _ _ => ltac:(reflexivity) |}.

(* FIXME: this proper-ness proof should include irrelevance of the OType arg *)
Instance Proper_const_ofun {A B} `{OType A} `{OType B} :
  Proper (oleq ==> oleq) (const_ofun (A:=A) (B:=B)).
Proof.
  intros b1 b2 Rb a1 a2 Ra. apply Rb.
Qed.

Instance Proper_const_ofun_equiv {A B} `{OType A} `{OType B} :
  Proper (oeq ==> oeq) (const_ofun (A:=A) (B:=B)).
Proof.
  intros b1 b2 Rb; split; intros a1 a2 Ra; apply Rb.
Qed.

(* Composing with the constant ofun on the left *)
Lemma compose_const_ofun_f A B C `{OType A} `{OType B} `{OType C}
      b (f : B -o> C) :
  oeq (compose_ofun (const_ofun (A:=A) b) f) (const_ofun (ofun_app f b)).
  split; intros a1 a2 Ra; reflexivity.
Qed.

(* Composing with the constant ofun on the right *)
Lemma compose_f_const_ofun A B C `{OType A} `{OType B} `{OType C}
      (f : A -o> B) c :
  oeq (compose_ofun f (const_ofun c)) (const_ofun c).
  split; intros a1 a2 Ra; reflexivity.
Qed.

(* Take the pair of the outputs of two ofuns *)
Program Definition pair_ofun {A B C}
        `{OType A} `{OType B} `{OType C}
        (f: A -o> B) (g: A -o> C) : A -o> (B * C) :=
  {| ofun_app := fun a => (ofun_app f a, ofun_app g a) |}.
Next Obligation.
  intros a1 a2 Ra; split; apply ofun_Proper; assumption.
Qed.

Instance Proper_pair_ofun A B C `{OType A} `{OType B} `{OType C} :
  Proper (oleq ==> oleq ==> oleq) (pair_ofun (A:=A) (B:=B) (C:=C)).
Proof.
  intros a1 a2 Ra b1 b2 Rb c1 c2 Rc; simpl; split.
  - apply Ra; assumption.
  - apply Rb; assumption.
Qed.

Instance Proper_pair_ofun_equiv A B C
         `{OType A} `{OType B} `{OType C} :
  Proper (oeq ==> oeq ==> oeq)
         (pair_ofun (A:=A) (B:=B) (C:=C)).
Proof.
  intros a1 a2 Ra b1 b2 Rb.
  destruct Ra as [ Ra1 Ra2 ]; destruct Rb as [ Rb1 Rb2 ].
  split; intros c1 c2 Rc; split; simpl;
    first [ apply Ra1 | apply Ra2 | apply Rb1 | apply Rb2 ]; assumption.
Qed.

(* compose commutes with pair *)
Lemma compose_f_pair_ofun A B C D
      `{OType A} `{OType B} `{OType C} `{OType D}
      (f: A -o> B) (g: B -o> C) (h: B -o> D) :
  oeq (compose_ofun f (pair_ofun g h))
           (pair_ofun (compose_ofun f g) (compose_ofun f h)).
  split; intros a1 a2 Ra; simpl; split; repeat apply ofun_Proper; assumption.
Qed.

(* The first projection ofun *)
Definition fst_ofun {A B} `{OType A} `{OType B} : A * B -o> A :=
  {| ofun_app := fst; ofun_Proper := _ |}.

(* The second projection ofun *)
Definition snd_ofun {A B} `{OType A} `{OType B} : A * B -o> B :=
  {| ofun_app := snd; ofun_Proper := _ |}.

(* Composing pair with fst gives the first function in the pair *)
Lemma compose_pair_fst A B C `{OType A} `{OType B} `{OType C}
      (f: A -o> B) (g: A -o> C) :
  oeq (compose_ofun (pair_ofun f g) fst_ofun) f.
  split; intros a1 a2 Ra; simpl; apply ofun_Proper; assumption.
Qed.

(* Composing pair with snd gives the second function in the pair *)
Lemma compose_pair_snd A B C `{OType A} `{OType B} `{OType C}
      (f: A -o> B) (g: A -o> C) :
  oeq (compose_ofun (pair_ofun f g) snd_ofun) g.
  split; intros a1 a2 Ra; simpl; apply ofun_Proper; assumption.
Qed.

(* Taking the pair of fst and snd is the identity *)
Lemma pair_fst_snd_eta A B `{OType A} `{OType B} :
  oeq (pair_ofun (fst_ofun (A:=A) (B:=B)) snd_ofun) id_ofun.
  split; intros p1 p2 Rp; destruct Rp; split; simpl; assumption.
Qed.

(* Curry an OFun *)
Program Definition ofun_curry {A B C} `{OType A} `{OType B} `{OType C}
        (ofun : (A * B) -o> C)
  : A -o> (B -o> C) :=
  {| ofun_app :=
       fun a =>
         {| ofun_app := fun b => ofun_app ofun (a,b);
            ofun_Proper := _ |};
     ofun_Proper := _ |}.
Next Obligation.
Proof.
  intros b1 b2 Rb. apply ofun_Proper.
  split; [ reflexivity | assumption ].
Qed.
Next Obligation.
Proof.
  intros a1 a2 Ra b1 b2 Rb; simpl.
  apply ofun_Proper; split; assumption.
Qed.

(* Uncrry an OFun *)
Program Definition ofun_uncurry {A B C}
        `{OType A} `{OType B} `{OType C}
        (ofun : A -o> (B -o> C))
  : (A * B) -o> C :=
  {| ofun_app :=
       fun ab => ofun_app (ofun_app ofun (fst ab)) (snd ab);
     ofun_Proper := _ |}.
Next Obligation.
Proof.
  intros ab1 ab2 Rab. destruct Rab as [ Ra Rb ].
  exact (ofun_Proper ofun (fst ab1) (fst ab2) Ra (snd ab1) (snd ab2) Rb).
Qed.

(* ofun_curry is Proper *)
Instance Proper_ofun_curry A B C `{OType A} `{OType B} `{OType C}
  : Proper (oleq ==> oleq) (ofun_curry (A:=A) (B:=B) (C:=C)).
Proof.
  intros f1 f2 Rf a1 a2 Ra b1 b2 Rb. apply Rf. split; assumption.
Qed.

(* ofun_curry is Proper w.r.t. equivalence *)
Instance Proper_ofun_curry_equiv A B C `{OType A} `{OType B} `{OType C} :
  Proper (oeq ==> oeq) (ofun_curry (A:=A) (B:=B) (C:=C)).
Proof.
  intros f1 f2 Rf; destruct Rf; split; apply Proper_ofun_curry; assumption.
Qed.

(* FIXME: Proper instance for ofun_uncurry *)

(* Currying and uncurrying of ofuns form an isomorphism: part 1 *)
Lemma ofun_curry_uncurry_eq A B C `{OType A} `{OType B} `{OType C}
      (f: (A * B) -o> C) :
  ofun_uncurry (ofun_curry f) =o= f.
  split; intros ab1 ab2 Rab; simpl; apply ofun_Proper;
    destruct Rab; split; assumption.
Qed.

(* Currying and uncurrying of ofuns form an isomorphism: part 2 *)
Lemma ofun_uncurry_curry_eq A B C `{OType A} `{OType B} `{OType C}
      (f: A -o> B -o> C) :
  ofun_curry (ofun_uncurry f) =o= f.
  split; intros a1 a2 Ra b1 b2 Rb; simpl; apply Proper_ofun_app;
    try apply ofun_Proper; assumption.
Qed.

(* The S combinator for ofuns (FIXME: do we need this?) *)
Program Definition ofun_S {A B C} `{OType A} `{OType B} `{OType C}
  : (A -o> B -o> C) -o> (A -o> B) -o> A -o> C :=
  {| ofun_app :=
       fun f =>
         {| ofun_app :=
              fun g =>
                {| ofun_app := fun a => ofun_app (ofun_app f a) (ofun_app g a) |}
         |}
  |}.
Next Obligation.
  intros a1 a2 Ra; apply Proper_ofun_app; try apply ofun_Proper; assumption.
Qed.
Next Obligation.
  intros g1 g2 Rg a1 a2 Ra. simpl. apply Proper_ofun_app; try assumption.
  - apply ofun_Proper; assumption.
  - apply Rg; assumption.
Qed.
Next Obligation.
  intros f1 f2 Rf g1 g2 Rg a1 a2 Ra. simpl. apply Proper_ofun_app; try assumption.
  - intros b1 b2 Rb. apply Rf; assumption.
  - apply Rg; assumption.
Qed.

(* This is the S combinator, but partially applied *)
Program Definition ofun_apply {A B C}
        `{OType A} `{OType B} `{OType C}
        (f: A -o> B -o> C) (g: A -o> B) : A -o> C :=
  {| ofun_app := fun a => ofun_app (ofun_app f a) (ofun_app g a) |}.
Next Obligation.
  intros a1 a2 Ra; apply Proper_ofun_app; try apply ofun_Proper; assumption.
Qed.

Instance Proper_ofun_apply A B C `{OType A} `{OType B} `{OType C} :
  Proper (oleq ==> oleq ==> oleq) (ofun_apply (A:=A) (B:=B) (C:=C)).
Proof.
  intros a1 a2 Ra b1 b2 Rb c1 c2 Rc. simpl.
  apply Ra; try assumption. apply Rb; try assumption.
Qed.

Instance Proper_ofun_apply_equiv A B C
         `{OType A} `{OType B} `{OType C} :
  Proper (oeq ==> oeq ==> oeq) (ofun_apply (A:=A) (B:=B) (C:=C)).
Proof.
  intros a1 a2 Ra b1 b2 Rb; split; intros c1 c2 Rc; simpl;
    apply Ra; try apply Rb; assumption.
Qed.

(* compose commutes with S *)
Lemma compose_ofun_apply A B C D `{OType A} `{OType B} `{OType C} `{OType D}
      (f : A -o> B) (g: B -o> C -o> D) h :
  compose_ofun f (ofun_apply g h)
  =o= ofun_apply (compose_ofun f g) (compose_ofun f h).
  split; intros a1 a2 Ra; simpl; rewrite Ra; reflexivity.
Qed.

(* compose commutes with currying *)
Lemma compose_ofun_curry A B C D `{OType A} `{OType B} `{OType C} `{OType D}
      (f: A -o> B) (g: B * C -o> D) :
  oeq (compose_ofun f (ofun_curry g))
           (ofun_curry
              (compose_ofun (pair_ofun (compose_ofun fst_ofun f) snd_ofun) g)).
  split; intros a1 a2 Ra c1 c2 Rc; simpl; rewrite Ra; rewrite Rc; reflexivity.
Qed.

(* Applying a const is just composition. Note that we add the extra OType
constraint to quantify over all possible proofs that B -o> C is an OType, so
this rule applies independently of this aOType proof. *)
Lemma ofun_apply_const A B C `{OType A} `{OType B} `{OType C}
      {OBC: OType (B -o> C)} (f: B -o> C) (g: A -o> B) :
  oeq (ofun_apply (A:=A) (const_ofun f) g) (compose_ofun g f).
  split; intros a1 a2 Ra; simpl; rewrite Ra; reflexivity.
Qed.

(* We can simplify ofun_S used with ofun_curry *)
Lemma ofun_apply_ofun_curry A B C `{OType A} `{OType B} `{OType C} f g :
  oeq (ofun_apply (A:=A) (B:=B) (C:=C) (ofun_curry f) g)
           (compose_ofun (pair_ofun id_ofun g) f).
  split; intros a1 a2 Ra; simpl; apply ofun_Proper; split;
    try apply ofun_Proper; assumption.
Qed.

(* The pair constructor as an ofun *)
Program Definition pair_ctor_ofun {A B} `{OType A} `{OType B}
  : A -o> B -o> A * B :=
  {| ofun_app := fun a => {| ofun_app := fun b => (a,b) |} |}.
Next Obligation.
  intros b1 b2 Rb; rewrite Rb; split; reflexivity.
Qed.
Next Obligation.
  intros a1 a2 Ra b1 b2 Rb; simpl; rewrite Ra; rewrite Rb; split; reflexivity.
Qed.

(* Applying pair_ctor_ofun yields a pair_ofun *)
Lemma apply_pair_ctor_ofun {A B C} `{OType A} `{OType B} `{OType C}
      (f: A -o> B) (g: A -o> C) :
  oeq (ofun_apply (ofun_apply (const_ofun pair_ctor_ofun) f) g)
           (pair_ofun f g).
  split; intros a1 a2 Ra; simpl; rewrite Ra; split; reflexivity.
Qed.

(***
 *** Building Proper Functions
 ***)

Class ProperPair A `{OType A} (x y:A) : Prop :=
  proper_pair_pf : oleq x y.

Class OFunProper {A B} `{OType A} `{OType B} (f: A -> B) : Prop :=
  ofun_proper : forall x y, ProperPair A x y -> ProperPair B (f x) (f y).

Hint Extern 1 (OFunProper _) => intro; intro; intro : typeclass_instances.

Definition mk_ofun {A B} `{OType A} `{OType B} (f: A -> B) {prp:OFunProper f}
  : A -o> B :=
  {| ofun_app := f; ofun_Proper := prp |}.

Notation "'ofun' x => e" := (mk_ofun (fun x => e))
                              (right associativity, at level 99).

Notation "'ofun' ( x : A ) => e" :=
  (mk_ofun (fun x:A => e))
    (right associativity, at level 99, x at level 0).

Instance ProperPair_refl A `{OType A} (x:A) : ProperPair A x x.
Proof.
  unfold ProperPair. reflexivity.
Qed.

Lemma ProperPair_ofun_app A B `{OType A} `{OType B}
      (fl fr:A -o> B) argl argr
      (prpf:ProperPair (A -o> B) fl fr)
      (prpa:ProperPair A argl argr)
 : ProperPair B (ofun_app fl argl) (ofun_app fr argr).
Proof.
  apply prpf; assumption.
Qed.

Lemma ProperPair_ofun A B `{OType A} `{OType B} (f g:A -> B) prpl prpr
         (pf: forall x y, ProperPair A x y -> ProperPair B (f x) (g y)) :
  ProperPair (A -o> B) (@mk_ofun A B _ _ f prpl) (@mk_ofun A B _ _ g prpr).
Proof.
  intros xl xr Rx; apply pf; assumption.
Qed.

Hint Extern 2 (ProperPair _ _ _) =>
first [ apply ProperPair_ofun_app
      | apply ProperPair_ofun; do 3 intro ] : typeclass_instances.

(*
Hint Extern 3 (ProperPair _ _ _) =>
lazymatch goal with
| |- ProperPair _ (ofun_app _ _) (ofun_app _ _) =>
  apply ProperPair_ofun_app
| |- ProperPair ?A (?f ?x) (?g ?y) =>
  let fapp := (eval beta in (f x)) in
  let gapp := (eval beta in (g y)) in
  change (ProperPair A fapp gapp)
| |- ProperPair (?A -o> ?B) (@ofun _ _ _ _ ?f ?prpf) (@ofun _ _ _ _ ?g ?prpg) =>
  let x := fresh "x" in
  let y := fresh "y" in
  let ppair := fresh "ppair" in
  apply ProperPair_ofun; intros x y ppair;
    let fapp := eval beta in (f x) in
    let gapp := eval beta in (g y) in
    change (ProperPair B fapp gapp)
end.
*)

(***
 *** Ordered Terms and ProperPair Instances for Pair Operations
 ***)

(* Proper function for fst *)
Definition ofst {A B} `{OType A} `{OType B} : A * B -o> A :=
  {| ofun_app := fst; ofun_Proper := _ |}.

(* Proper function for snd *)
Definition osnd {A B} `{OType A} `{OType B} : A * B -o> B :=
  {| ofun_app := snd; ofun_Proper := _ |}.

(* Proper function for pair *)
Program Definition opair {A B} `{OType A} `{OType B} : A -o> B -o> A * B :=
  {| ofun_app :=
       fun a => {| ofun_app := fun b => pair a b;
                   ofun_Proper := _ |};
     ofun_Proper := _ |}.
Next Obligation.
  intros b1 b2 Rb. split; [ reflexivity | assumption ].
Qed.
Next Obligation.
  intros a1 a2 Ra b1 b2 Rb. split; assumption.
Qed.

(* Notation for proper pairs *)
Notation "( x ,o, y )" := (opair @o@ x @o@ y) (at level 0).

(* FIXME: get this notation to work *)
(*
Notation "( x ,o, y ,o, .. ,o, z )" :=
  (ofun_app opair .. (ofun_app (ofun_app opair x) y) .. z)
                                         (at level 0).
*)

(*
Instance ProperPair_fst A B `{OType A} `{OType B} (p1 p2: A*B)
         (pf: ProperPair (A*B) p1 p2) :
  ProperPair A (fst p1) (fst p2).
Proof.
  destruct pf; assumption.
Qed.

Instance ProperPair_snd A B `{OType A} `{OType B} (p1 p2: A*B)
         (pf: ProperPair (A*B) p1 p2) :
  ProperPair B (snd p1) (snd p2).
Proof.
  destruct pf; assumption.
Qed.

Instance ProperPair_pair A B `{OType A} `{OType B}
         (x1 x2:A) (y1 y2:B) (pfx: ProperPair A x1 x2) (pfy: ProperPair B y1 y2) :
  ProperPair (A*B) (pair x1 y1) (pair x2 y2).
Proof.
  split; assumption.
Qed.
 *)

(***
 *** Ordered Terms for Sum Operations
 ***)

(* Proper function for inl *)
Program Definition oinl {A B} `{OType A} `{OType B} : A -o> A + B :=
  {| ofun_app := inl; ofun_Proper := _ |}.
Next Obligation.
  intros x y Rxy. left. assumption.
Defined.

(* Proper function for inr *)
Program Definition oinr {A B} `{OType A} `{OType B} : B -o> A + B :=
  {| ofun_app := inr; ofun_Proper := _ |}.
Next Obligation.
  intros x y Rxy. right. assumption.
Defined.

(* Proper function for eliminating sums *)
Program Definition osum_elim {A B C} `{OType A} `{OType B} `{OType C} :
  (A -o> C) -o> (B -o> C) -o> A + B -o> C :=
  {| ofun_app :=
       fun f1 =>
         {| ofun_app :=
              fun f2 =>
                {| ofun_app := fun (s : A+B) =>
                                 match s return C with
                                 | inl a => f1 @o@ a
                                 | inr b => f2 @o@ b
                                 end |} |} |}.
Next Obligation.
  intros s1 s2 Rs. destruct Rs; apply ofun_Proper; assumption.
Defined.
Next Obligation.
  intros f2 f2' Rf2 a1 a2 Ra. destruct Ra; simpl.
  - apply ofun_Proper; assumption.
  - apply Rf2; assumption.
Defined.
Next Obligation.
  intros f1 f1' Rf1 f2 f2' Rf2 a1 a2 Ra. destruct Ra; simpl.
  - apply Rf1; assumption.
  - apply Rf2; assumption.
Defined.

Lemma osum_elim_eta  {A B} `{OType A} `{OType B} :
  osum_elim (A:=A) (B:=B) @o@ oinl @o@ oinr =o= id_ofun.
Proof.
  split; intros s1 s2 Rs; destruct Rs; simpl; constructor; assumption.
Qed.

(***
 *** Ordered Terms for Boolean Operations
 ***)

Program Definition oif {A} `{OType A} : bool -o> A -o> A -o> A :=
  mk_ofun
    (fun (b:bool) =>
       mk_ofun
         (fun x =>
            mk_ofun
              (fun y => if b then x else y) (prp:=_)) (prp:=_)) (prp:=_).
Next Obligation.
  unfold OFunProper, ProperPair; intros a1 a2 Ra.
  destruct b; [ reflexivity | apply Ra ].
Defined.
Next Obligation.
  unfold OFunProper, ProperPair; intros a1 a2 R12 a3 a4 R34.
  destruct b; [ apply R12 | assumption ].
Defined.
Next Obligation.
  unfold OFunProper, ProperPair; simpl; intros.
  destruct x; destruct y; try discriminate; assumption.
Defined.

(***
 *** Ordered Terms for Propositional Connectives
 ***)

(* The universal combinator as an ordered function *)
Program Definition oforall `{OType} : (A -o> Prop) -o> Prop :=
  mk_ofun (fun (P:A -o> Prop) => forall x, P @o@ x) (prp:=_).
Next Obligation.
  intros P1 P2 R12 pf z. apply (R12 _ _ (reflexivity _) (pf z)).
Defined.

(* The existential combinator as an ordered function *)
Program Definition oexists `{OType} : (A -o> Prop) -o> Prop :=
  mk_ofun (fun P => exists x, P @o@ x) (prp:=_).
Next Obligation.
  intros P1 P2 R12 pf. destruct pf as [z pf].
  exists z. apply (R12 _ _ (reflexivity _) pf).
Defined.

(* The double existential combinator as an ordered function *)
Program Definition oexists2 `{OType} : (A -o> Prop) -o> (A -o> Prop) -o> Prop :=
  mk_ofun
    (fun P =>
       mk_ofun
         (fun Q => exists2 x, P @o@ x & Q @o@ x) (prp:=_)) (prp:=_).
Next Obligation.
  intros P1 P2 R12 pf. destruct pf as [z pf1 pf2].
  exists z; try assumption. apply (R12 _ _ (reflexivity _) pf2).
Defined.
Next Obligation.
  intros P1 P2 RP Q1 Q2 RQ pf. destruct pf as [z pf1 pf2].
  exists z; [ apply (RP _ _ (reflexivity _) pf1)
            | apply (RQ _ _ (reflexivity _) pf2) ].
Defined.

(* Conjunction as an ordered function *)
Program Definition oand : Prop -o> Prop -o> Prop :=
  mk_ofun (fun P1 => mk_ofun (fun P2 => P1 /\ P2) (prp:=_)) (prp:=_).
Next Obligation.
  intros P2' P2'' R2 H0. destruct H0; split; try assumption.
  apply R2; assumption.
Defined.
Next Obligation.
  intros P1 P1' R1 P2 P2' R2 H0. destruct H0.
  split; [ apply R1 | apply R2 ]; assumption.
Defined.

(* Disjunction as an ordered function *)
Program Definition oor : Prop -o> Prop -o> Prop :=
  mk_ofun (fun P1 => mk_ofun (fun P2 => P1 \/ P2) (prp:=_)) (prp:=_).
Next Obligation.
  intros P2' P2'' R2 H0.
  destruct H0; [ left | right; apply R2 ]; assumption.
Defined.
Next Obligation.
  intros P1 P1' R1 P2 P2' R2 H0.
  destruct H0; [ left; apply R1 | right; apply R2 ]; assumption.
Defined.

(* Implication as an ordered function *)
Program Definition oimpl : Flip Prop -o> Prop -o> Prop :=
  mk_ofun (fun (P1:Flip Prop) =>
             mk_ofun (fun (P2:Prop) =>
                        unflip P1 -> P2) (prp:=_)) (prp:=_).
Next Obligation.
  intros P2 P2' R2 pf12 pf1.
  apply R2; apply pf12; apply pf1; assumption.
Defined.
Next Obligation.
  intros P1 P1' R1 P2 P2' R2 pfx1 pfy.
  apply R2; apply pfx1; apply R1; apply pfy.
Defined.

(* Ordered type relations are themselves ordered propositional functions *)
Program Definition oR `{OType} : Flip A -o> A -o> Prop :=
  mk_ofun (fun (x:Flip A) =>
             mk_ofun (fun y => oleq (unflip x) y) (prp:=_)) (prp:=_).
Next Obligation.
  intros a1 a2 Ra pf. etransitivity; eassumption.
Defined.
Next Obligation.
  intros a1 a2 R12 a3 a4 R34; simpl; intro pf.
  etransitivity; try eassumption.
  etransitivity; try eassumption.
  apply R12.
Defined.

(***
 *** Notations for Ordered Terms
 ***)

(* FIXME: why don't these work?
Notation "'ofun' ( x : A ) =o> t" :=
  (@ot_Lambda A _ (fun x => t))
    (at level 100, right associativity, x at level 99) : pterm_scope.

Notation "'ofun' x =o> t" :=
  (ot_Lambda (fun x => t))
    (at level 100, right associativity, x at level 99) : pterm_scope.
 *)

(***
 *** Unary Ordered Type Functors
 ***)

(* Typeclass version of OTypeF1Fun *)
Class OTypeF1 (F:forall A {RA:OType A}, Type) : Type :=
  otypeF1 : forall A {RA:OType A}, OType (F A).

(* Get out the OType from applying a unary functor *)
Instance OType_OTypeF1 F (RF:OTypeF1 F) A (RA:OType A) :
  OType (F A _) | 5 := RF A _.

Typeclasses Transparent OType_OTypeF1.

(* Typeclass for finding a unary OType function *)
(*
Class FindOTypeF1 (F:forall A {RA:OType A}, Type)
      (RF: forall A {RA:OType A}, OType (F A)) : Prop :=
  findOTypeF1 : True.

Ltac findOTypeF1 :=
  lazymatch goal with
  | |- OType (?F ?A ?RA) =>
    let RF := fresh "RF" in
    evar (RF: forall A' (RA':OType A'), OType (F A'));
    assert (FindOTypeF1 F ?RF); [ | apply (RF A RA) ]
  end.
*)

(***
 *** Examples of Ordered Terms
 ***)

Module OTExamples.

Definition ex1 : Prop -o> Prop := ofun p => p.
(* Eval compute in (ofun_app ex1 : Prop -> Prop). *)

Definition ex2 {A} `{OType A} : A -o> A := ofun p => p.
(* Eval simpl in (fun A `{OType A} => ofun_app (@ex2 A _) : A -> A). *)

Definition ex3 {A} `{OType A} : A -o> A -o> A :=
  ofun p1 => ofun p2 => p1.
(* Eval simpl in (fun A `{OType A} x =>
                 ofun_app (ofun_app (@ex3 A _) x)). *)

Definition ex4 {A B} `{OType A} `{OType B} : (A * B -o> A) :=
  ofun p => ofst @o@ p.
(* Eval simpl in (fun {A B} `{OType A} `{OType B} =>
                 ofun_app ex4 : A * B -> A). *)

Definition ex5 {A B} `{OType A} `{OType B} : A * B -o> B * A :=
  ofun p => (osnd @o@ p ,o, ofst @o@ p).
(* Eval simpl in (fun {A B} `{OType A} `{OType B} =>
                 ofun_app ex5 : A * B -> B * A). *)

Definition ex6 {A B C} `{OType A} `{OType B} `{OType C} : A * B * C -o> C * A :=
  ofun triple => (osnd @o@ triple ,o, ofst @o@ (ofst @o@ triple)).
(* Eval simpl in (fun {A B} `{OType A} `{OType B} =>
                 ofun_app ex5 : A * B -> B * A). *)

Definition ex7 {A B C} `{OType A} `{OType B} `{OType C}
  : (A * B -o> C) -o> C -o> A -o> B -o> C :=
  ofun f => ofun c =>
  ofun a => ofun b => f @o@ (a ,o, b).

End OTExamples.

author: eddywestbrook

repo: predicate-monads


text:
Load LFindLoad.
From lfind Require Import LFind.
Unset Printing Notations.
Set Printing Implicit.

From QuickChick Require Import QuickChick.
Inductive natural : Type := Succ : natural -> natural |  Zero : natural.
Derive Show for natural. Derive Arbitrary for natural.  Instance Dec_Eq_natural : Dec_Eq natural. Proof. dec_eq. Qed.
Inductive lst : Type :=  Nil : lst | Cons : natural -> lst -> lst .

Inductive tree : Type := Node : natural -> tree -> tree -> tree |  Leaf : tree.

Inductive Pair : Type := mkpair : natural -> natural -> Pair
with Zlst : Type := zcons : Pair -> Zlst -> Zlst |  znil : Zlst.

Fixpoint append (append_arg0 : lst) (append_arg1 : lst) : lst
           := match append_arg0, append_arg1 with
              | Nil, x => x
              | Cons x y, z => Cons x (append y z)
              end.

Fixpoint rev (rev_arg0 : lst) : lst
           := match rev_arg0 with
              | Nil => Nil
              | Cons x y => append (rev y) (Cons x Nil)
              end.

Lemma append_nil : forall (x : lst), append x Nil = x.
Proof.
   intros.
   induction x.
   - reflexivity.
   - simpl. rewrite IHx. reflexivity.
Qed.

Lemma append_assoc : forall (x y z : lst), append (append x y) z = append x (append y z).
Proof.
   intros.
   induction x.
   - reflexivity.
   - simpl. rewrite IHx. reflexivity.
Qed.

Lemma rev_append : forall (x y : lst), rev (append x y) = append (rev y) (rev x).
Proof.
   intros.
   induction x.
   - simpl. rewrite append_nil. reflexivity.
   - simpl. rewrite IHx. rewrite append_assoc. reflexivity.
Qed.

Lemma rev_rev : forall (x : lst), rev (rev x) = x.
Proof.
   intros.
   induction x.
   - reflexivity.
   - simpl. lfind.  simpl.  rewrite IHx.  reflexivity.
Admitted.

Theorem theorem0 : forall (x : lst) (y : lst), eq (rev (append (rev x) (rev y))) (append y x).
Proof.
   induction x.
   - intros. simpl. rewrite rev_rev. rewrite append_nil. reflexivity.
   - intros. simpl. rewrite rev_append. simpl. rewrite (eq_refl : Cons n Nil = rev (Cons n Nil)). rewrite IHx. rewrite rev_rev. simpl. reflexivity.
Qed.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import compcert.lib.Integers.
Require Import compcert.lib.Axioms.
From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype seq.
Require Import Lists.List.
Require Import Coq.ZArith.ZArith.
Require Import PreOmega.
Set Implicit Arguments.
Import Axioms.
(* tactics to support Omega for ssrnats*)
Ltac arith_hypo_ssrnat2coqnat :=
  match goal with
    | H : context [andb _ _] |- _ => let H0 := fresh in case/andP: H => H H0
    | H : context [orb _ _] |- _ => case/orP: H => H
    | H : context [?L <= ?R] |- _ => move/leP: H => H
    | H : context [?L < ?R] |- _ => move/ltP : H => H
    | H : context [?L == ?R] |- _ => move/eqP : H => H
    | H : context [addn ?L ?R] |- _ => rewrite -plusE in H
    | H : context [muln ?L ?R] |- _ => rewrite -multE in H
    | H : context [subn ?L ?R] |- _ => rewrite -minusE in H
  end.

Ltac arith_goal_ssrnat2coqnat :=
  rewrite ?NatTrec.trecE -?plusE -?minusE -?multE -?leqNgt -?ltnNge;
  repeat match goal with
           | |- is_true (andb _ _) => apply/andP; split
           | |- is_true (orb _ _) => try apply/orP
           | |- is_true (_ <= _) => try apply/leP
           | |- is_true (_ < _) => try apply/ltP
         end.

Ltac ssromega :=
  repeat arith_hypo_ssrnat2coqnat;
  arith_goal_ssrnat2coqnat; simpl;
  omega.

Class monad (mon : Type -> Type) :=
  {
    ret : forall {A : Type},  A -> mon A;
    bind : forall {A B : Type}, mon A -> (A -> mon B) -> mon B
  }.

Notation "x >>= f" := (bind x f) (at level 40, left associativity).
Notation "'do!' X <- A ; B" := (bind A (fun X => B)) (at level 40).

Lemma if_true : forall {A : Type} b (x y : A)
                  (Htrue: is_true b),
                  (if b then x else y) = x.
Proof.
  intros. now rewrite Htrue.
Defined.

Lemma if_false : forall {A : Type} b (x y : A)
                   (Hfalse: is_true (~~b)),
                   (if b then x else y) = y.
Proof.
  intros. rewrite <- Bool.if_negb. by rewrite Hfalse.
Defined.

Lemma not_in_filter :
  forall {A:eqType} (i : A) xs
    (HIn: ~ List.In i xs),
    [seq x <- xs | x == i] = [::].
Proof.
  intros.
  induction xs as [|j xs]; first by reflexivity.
  simpl.
  destruct (j == i) eqn:Hji; move/eqP:Hji=>Hji;
    first by (subst j; simpl in *; exfalso; apply HIn; by auto).
  apply IHxs. intros Hcontra.
  apply HIn. simpl; by auto.
Qed.

Lemma nth_error_app_inv:
  forall (A : Type) (i : nat) (v: A) (ys xs : seq.seq A), nth_error xs i = Some v ->
                                                   nth_error (xs ++ ys) i = Some v.
  intros.
  generalize dependent i.
  generalize dependent v.
  induction xs;
    intros.
  rewrite Coqlib.nth_error_nil in H.
  discriminate.
  destruct i; simpl in *;
    now auto.
Qed.

Lemma app_eq_refl_nil:
  forall {A:Type} (xs ys : list A),
    xs = xs ++ ys ->
    ys = nil.
Proof.
  intros.
  erewrite <- app_nil_r in H at 1.
  apply app_inv_head in H; auto.
Qed.

Lemma app_assoc_l:
  forall (A : Type) (l m n : seq.seq A),
    l ++ m ++ n = l ++ (m ++ n).
Proof.
  intros;
    by rewrite app_assoc.
Qed.

Lemma filter_neq_eq :
  forall {A :eqType} (xs : seq.seq A) i j (Hneq: i <> j),
    [seq x <- [seq x <- xs | x != i] | x == j] = [seq x <- xs | x == j].
Proof.
  intros. induction xs.
  - reflexivity.
  - simpl. destruct (a != i) eqn:Hai; move/eqP:Hai=>Hai.
    simpl.
    destruct (a ==j) eqn:Haj; move/eqP:Haj=>Haj;
                                             [by apply f_equal | assumption].
    subst. erewrite if_false by (apply/eqP; auto).
    assumption.
Qed.

Lemma nth_error_app:
  forall {A:Type} i (ys xs : list A),
    nth_error xs i = nth_error (ys ++ xs) (length ys + i).
Proof.
  intros A i ys.
  generalize dependent i.
  induction ys; intros.
  - simpl. rewrite add0n.
    reflexivity.
  - simpl.
    eauto.
Qed.

Lemma list_cons_irrefl:
  forall {A: Type} (x : A) xs,
    ~ x :: xs = xs.
Proof.
  intros.
  induction xs; intro Hcontra; simpl; try discriminate.
  inversion Hcontra; subst a; auto.
Qed.

Lemma lt_succ_neq:
  forall x y z,
    (x <= y < x + Z.succ z)%Z ->
    y <> (x + z)%Z ->
    (x <= y < x + z)%Z.
Proof.
  intros.
  omega.
Qed.

Lemma le_sub:
  forall x y z,
    (x < z)%positive ->
    (z <= y)%positive ->
    (x <= Z.to_pos (Z.pos_sub y (z - x)))%positive.
Proof.
  intros x y z H H0.
  zify.
  rewrite <-Pos2Z.add_pos_neg.
  assert (x < z)%positive by auto.
  rewrite Z2Pos.id; zify; omega.
Qed.

Lemma lt_sub_bound:
  forall x y,
    (x < y)%positive ->
    (Z.to_pos (Z.pos_sub y (y - x)) < Pos.succ x)%positive.
Proof.
  intros x y H.
  zify.
  rewrite <-Pos2Z.add_pos_neg.
  rewrite Z2Pos.id; zify; omega.
Qed.

Lemma lt_lt_sub:
  forall a b c,
    (a < b)%positive ->
    (b <= c)%positive ->
    (b - a < c)%positive.
Proof.
  intros a b c H H0.
  zify; omega.
Qed.

Lemma prod_fun :
  forall {A B C : Type}
    (f g: A -> (B * C)),
    f = g ->
    (fun x : A => fst (f x)) =  (fun x : A => fst (g x)) /\
    (fun x : A => snd (f x)) = (fun x : A => snd (g x)).
Proof.
  intros.
  assert ((fun x => fst (f x)) = (fun x => fst (g x))).
    by (eapply extensionality; intros x;
         pose (f x);
         pose (g x);
           by subst).
  assert ((fun x => snd (f x)) = (fun x => snd (g x)))
    by (eapply extensionality; intros x;
         pose (f x);
         pose (g x);
           by subst).
  rewrite H0 H1.
    by split.
Qed.

Lemma forall_and:
  forall {A : Type} (f g : A -> Prop),
    (forall x : A, f x /\ g x) <->
    (forall x : A, f x) /\ (forall x : A, g x).
Proof.
  intros. split; intros.
  split; intros; [eapply (proj1 (H x))| eapply (proj2 (H x))].
  destruct H; eauto.
Qed.

Lemma forall2_and:
  forall {A B : Type} (f g : A -> B -> Prop),
    (forall x y, f x y /\ g x y) <->
    (forall x y, f x y) /\ (forall x y, g x y).
Proof.
  intros.
  split; intros.
  split; intros; [eapply (proj1 (H x y)) | eapply (proj2 (H x y))].
  destruct H; eauto.
Qed.

Definition proj_sumbool_is_false : forall (P : Prop) (a : {P} + {~ P}), ~ P -> Coqlib.proj_sumbool a = false.
Proof.
  intros.
  unfold Coqlib.proj_sumbool.
  destruct a; auto; try by exfalso.
Qed.

Module BlockList.
  Import ListNotations.

  Fixpoint mkBlockList (n : nat) : list nat :=
    match n with
      | 0 => nil
      | S 0 => nil
      | S n =>  n :: (mkBlockList n)
    end.

  Lemma mkBlockList_unfold : forall n (Hn: n > 1),
                               n :: (mkBlockList n) = mkBlockList (S n).
  Proof.
    intros; simpl; destruct n. exfalso; auto.
    reflexivity.
  Qed.

  Lemma mkBlockList_unfold' : forall n,
                                (S n) :: (mkBlockList (S n)) = mkBlockList (S (S n)).
  Proof.
    intros; reflexivity.
  Qed.

  Lemma mkBlockList_include : forall n k (Hk: k > 0) (Hineq: k < n) (Hn: n > 1),
                                List.In k (mkBlockList n).
  Proof.
    intros n.
    induction n;
      intros.
    simpl. ssromega.
    destruct n. ssromega.
    rewrite <- mkBlockList_unfold'. simpl. simpl in IHn.
    destruct (beq_nat k (S n)) eqn:?. apply beq_nat_true in Heqb. subst.
    now left.
    right. apply IHn; auto;  clear IHn.
    apply beq_nat_false in Heqb. ssromega.
    apply beq_nat_false in Heqb. ssromega.
  Qed.

  Lemma mkBlockList_not_in : forall n m
                               (Hge: m >= n)
                               (HIn: List.In m (mkBlockList n)),
                               False.
  Proof.
    intros.
    destruct n. auto.
    destruct n. auto. generalize dependent m.
    induction n; intros. simpl in HIn. destruct HIn; subst; auto.
    rewrite <- mkBlockList_unfold' in HIn.
    apply List.in_inv in HIn. destruct HIn as [? | HIn]; subst.
    rewrite ltnn in Hge. auto.
    eapply IHn. Focus 2. eauto.
    eapply leq_ltn_trans; eauto.
  Qed.

  Lemma mkBlockList_range:
    forall n k
      (HIn: List.In k (mkBlockList (S (S n)))),
      k < (S (S n)) /\ k > 0.
  Proof.
    intro n. induction n; intros. simpl in HIn.
    destruct HIn; subst; auto.
    rewrite <- mkBlockList_unfold' in HIn.
    apply List.in_inv in HIn.
    destruct HIn as [? | HIn]; subst.
    auto. apply IHn in HIn. destruct HIn. auto.
  Qed.

End BlockList.

(*
Module SeqLemmas.

  Definition subSeq {T:eqType} (s1 s2 : seq T) :=
    drop ((size s2)-(size s1)) s2 == s1.

  Lemma dropS:
    forall {T:Type} n (x:T) l l'
      (Hdrop: drop n l = x :: l'), drop n.+1 l = l'.
  Proof.
    intros. generalize dependent n.
    induction l; intros. simpl in *. discriminate.
    simpl in *. destruct n. inversion Hdrop; subst. apply drop0.
    eapply IHl; eassumption.
  Defined.

  Lemma drop_size_lt : forall {T : Type} (s s' : seq T) n
                         (Hdrop: drop n s = s'),
                         size s >= size s'.
  Proof.
    intros T s. induction s; intros.
    destruct n; simpl in Hdrop; rewrite <- Hdrop; auto.
    simpl in *. destruct n. rewrite <- Hdrop. auto.
    eapply IHs in Hdrop. ssromega.
  Defined.
  Lemma subSeq_det : forall {T:eqType} (s s' s'' : seq T) (Hsize: size s' = size s'')
                       (Hsub': subSeq s' s) (Hsub'': subSeq s'' s),
                       s' = s''.
  Proof.
    intros T s. induction s; intros.
    - unfold subSeq in *. simpl in *. move/eqP:Hsub'=>Hsub'. subst. move/eqP:Hsub''; auto.
    - unfold subSeq in Hsub', Hsub''. simpl in Hsub', Hsub''.
      rewrite Hsize in Hsub'.
      destruct ((size s).+1 - size s'') eqn:Heq.
      move/eqP:Hsub''. move/eqP:Hsub'. intros. destruct s'; inversion Hsub'; subst.
      reflexivity.
      apply IHs. assumption.
      unfold subSeq.
        by replace n with (size s - size s') in Hsub' by ssromega.
          by replace n with (size s - size s'') in Hsub'' by ssromega.
  Defined.

  Lemma in_rcons : forall {T:Type} x y (s : seq T) (HIn: List.In x (rcons s y)),
                     x = y \/ List.In x s.
  Proof.
    intros. induction s.
    - simpl in HIn. destruct HIn; auto.
      simpl in HIn. destruct HIn as [|HIn]; subst.
      right. simpl. left. reflexivity.
      apply IHs in HIn. destruct HIn; subst; auto.
      right. simpl. auto.
  Defined.

  Lemma in_rcons_refl : forall {T:Type} x (s : seq T),
                          List.In x (rcons s x).
  Proof.
    intros. induction s. simpl. by left.
    simpl. by right.
  Defined.

  Lemma in_rcons_weaken:
    forall {T:Type} x y (s : seq T) (HIn: List.In x s),
      List.In x (rcons s y).
  Proof.
    intros. induction s.
    - inversion HIn.
    - inversion HIn; subst. simpl. by left.
      simpl. right. auto.
  Defined.

End SeqLemmas.
 *)

author: PrincetonUniversity

repo: VST


text:
From Coq Require Import FSets Arith List. Import ListNotations.
From QuickChick Require Import QuickChick. Import QcNotation.

Require Export ExtLib.Structures.Monads.
Export MonadNotation. Open Scope monad_scope.

Require Import String. Local Open Scope string.
(****************************************************************)

(* set of nats between 1 and n (representing nodes), no repeats *)
Module FSet := Make Nat_as_OT.

(* useful operations
- FSet.empty : the empty set
- FSet.is_empty s
- FSet.add x s : insert an element
- union s1 s2
- subset s1 s2 : returns true if s1 <= s2
- mem : membership
 *)

Instance showFSet : Show FSet.t :=
  {| show s := show (FSet.elements s)
  |}.
Compute (show (FSet.add 1 FSet.empty)).

Fixpoint all_nodes (n: nat) : FSet.t :=
  match n with
  | O => FSet.empty
  | S n' => FSet.add n' (all_nodes n')
  end.

(* Example of a network with 5 nodes *)
Definition nodes5 := all_nodes 5.
Compute FSet.elements nodes5.
(* Returns a list [0, 1, 2, 3, 4] *)

(* some examples from StackOverflow *)
Definition test := FSet.union (FSet.singleton 42)
                           (FSet.empty).

(* membership *)
Compute FSet.mem 0 test.   (* evaluates to `false` *)
Compute FSet.mem 42 test.  (* evaluates to `true`  *)

Compute FSet.is_empty test.     (* evaluates to `false` *)
Compute FSet.is_empty FSet.empty.  (* evaluates to `true` *)

(*now to build our generator! first, some familiar helper functions *)

(* straight from QC.v *)
Fixpoint genListSized {A} (sz : nat) (g : G A) : G (list A) :=
  match sz with
    | O => ret nil
    | S sz' =>
        freq [ (1, ret nil) ;
               ((Nat.square sz), liftM2 cons g (genListSized sz' g))
             ]
  end.

(* the following sometimes responds
   [Warning: The following logical axioms were encountered...]
   which Leo says not to worry about*)
(*generates lists of length up to len, w elts that are nats < n*)
Definition genNatListSized (n : nat) (len : nat) : G (list nat) :=
  genListSized len (choose (0,n)).

(* Sample (genNatListSized 5 2).*)

Fixpoint genNatListSized' (n : nat) (len : nat) : G (list nat) :=
  match len with
    | O => ret nil
    | S len' =>
        freq [ (1, ret nil) ;
               (len, liftM2 cons (choose (0,n)) (genNatListSized n len'))
             ]
  end.
(*Sample (genNatListSized' 5 2).*)

(* basically [fold] from Poly.v*)
Fixpoint FSetFold (f: nat->FSet.t->FSet.t) (l: list nat) (b: FSet.t)
                         : FSet.t :=
  match l with
  | nil => b
  | h :: t => f h (FSetFold f t b)
  end.

(* Compute (show (FSetFold FSet.add [1;2;3] FSet.empty)).*)

(* function converting a list of nats to an FSet *)
Fixpoint listNatToFSet (l : list nat) : FSet.t :=
  FSetFold FSet.add l FSet.empty.

(* generator for FSets, takes *)
Fixpoint genFSet (n : nat) (len : nat) : G FSet.t :=
  (* n: elements can be any nat less than n *)
  (* len: max size of the FSets *)
  liftM listNatToFSet (genListSized len (choose (0,n))).

(*Sample (genFSet 5 2).*)

(****************************************************************)

(* set of sets of nodes, i.e. sets of FSets *)
Module FSys := Make FSet.

Instance showFSys: Show FSys.t :=
  {| show s := show (FSys.elements s)
  |}.

(* some examples *)
Definition test2 := FSys.union (FSys.singleton test) (FSys.empty).

Compute FSys.mem test test2. (* evaluates to `true` *)
Compute FSys.subset FSys.empty test2. (* evaluates to `true` *)

(*now we're ready to make our FSys generator!*)

Fixpoint genFSys (n : nat) (len : nat) (sys_sz : nat) : G FSys.t :=
  (*sys_sz: number of FSets in a generated FSys*)
  match sys_sz with
  | 0 => ret FSys.empty
  | S sys_sz' =>
    liftM2 FSys.add (genFSet n len) (genFSys n len sys_sz')
  end.

(* optionally, slightly more interesting generator *)
Fixpoint genFSys' (n : nat) (len : nat) (sys_sz : nat) : G FSys.t :=
  (*sys_sz: max number of FSets in a generated FSys*)
  match sys_sz with
  | 0 => ret FSys.empty
  | S sys_sz' =>
    freq [ (1, ret FSys.empty) ;
           ((Nat.square sys_sz), liftM2 FSys.add (genFSet n len) (genFSys n len sys_sz'))
               ]
  end.

(* Sample (genFSys 3 3 3).*)
(* Sample (genFSys 5 3 3).*)
(****************************************************************)

(* useful QuickChick types from QC.v, repeated here for convenience:

Inductive Result :=
  | Success : Result
  | Failure : forall {A} `{Show A}, A -> Result.

Arguments Failure {A} {H} _.

Instance showResult : Show Result :=
  {
    show r := match r with
              | Success => "Success"
              | Failure a => "Failure: " ++ show a (* edited from _ _ a*)
              end
  }.

Definition Checker := G Result.

Class Checkable A :=
  {
    checker : A -> Checker
  }.

Instance showUnit : Show unit :=
  {
    show u := "tt"
  }.

(** The failure cases in the [bool] and [Dec] checkers don't need to
    record anything except the [Failure], so we put [tt] (the sole
    value of type [unit]) as the "failure reason." *)

Instance checkableBool : Checkable bool :=
  {
    checker b := if b then ret Success else ret (Failure tt)
  }.

Instance checkableDec `{P : Prop} `{Dec P} : Checkable P :=
  {
    checker p := if P? then ret Success else ret (Failure tt)
  }.

(* Slightly modified to take an additional generator *)
Definition forAll {A B C : Type} `{Show A} `{Checkable C}
                  (ga : G A) (gb : G B) (f : A -> B -> C)
                : Checker :=
  a <- ga ;;
  b <- gb ;;
  r <- checker (f a b) ;;
  match r with
  | Success => ret Success
  | @Failure _ _ b => ret (Failure (a,b))
  end.
 *)

(****************************************************************)
(* properties to test *)
Definition q3 (f1 f2 f3 : FSet.t) (F : FSys.t) (n : nat) : bool :=
  (FSys.mem f1 F) && (FSys.mem f2 F) && (FSys.mem f3 F) &&
  negb  (FSet.subset (all_nodes n) (FSet.union (FSet.union f1 f2) f3)).
(* intuition: q3 is a property necessary for system-wide consistency,
    which says that no 3 fail sets in the system cover all nodes.*)

Definition q3all (F : FSys.t) (n : nat) :=
  forall f1 f2 f3, is_true (q3 f1 f2 f3 F n).

Definition q3all' (f1 f2 f3 : FSet.t) (F : FSys.t) (n : nat) :=
  (q3 f1 f2 f3 F n).

(****************************************************************)

(* chooseFSet: given FSys, this is a generator that chooses
     one FSet in FSys. *)
Check FSys.elements.
Definition chooseFSet (fsys : FSys.t) : G FSet.t :=
  elems_ FSet.empty (FSys.elements fsys).

(* genTriples: given FSys, this is a generator that will
   repeatedly choose 3 FSets in FSys at random,
   and returns a list of k such triples. *)
Fixpoint genTestTriples (k : nat) (fsys : FSys.t)
  : G (list (FSet.t*FSet.t*FSet.t)) :=
  let g3 :=
      f1 <- (chooseFSet fsys) ;;
         f2 <- (chooseFSet fsys) ;;
         f3 <- (chooseFSet fsys) ;;
      ret (f1,f2,f3) in
  vectorOf k g3.

(*********
   usage: replace n, len, sys_sz in the query below with desired parameters
  output: if there are 3 sets f1 f2 f3 in F that cover 0..n,
          print f1 f2 f3

QuickChick
  (forAll (genFSys n len sys_sz) (fun fs =>
      forAll (genTestTriples list_len fs) (fun l =>
           whenFail
            (String.concat "" (List.map (fun '(f1,f2,f3) =>
                                      if  (negb (q3 f1 f2 f3 fs n))
                                      then (show ("failed FSet:",f1,f2,f3))
                                      else "") l))
            (List.forallb (fun '(f1,f2,f3) =>  ( (q3 f1 f2 f3 fs n))) l)))).
*)

(*the following call to QuickChick will sometimes generate an empty system;
  just try calling it again.*)
QuickChick
  (forAll (genFSys 5 3 3) (fun fs =>
      forAll (genTestTriples 5 fs) (fun l =>
           whenFail
            (String.concat "" (List.map (fun '(f1,f2,f3) =>
                                      if  (negb (q3 f1 f2 f3 fs 5))
                                      then (show ("failed FSet:",f1,f2,f3))
                                      else "") l))
            (List.forallb (fun '(f1,f2,f3) =>  ( (q3 f1 f2 f3 fs 5))) l)))).

author: nglaeser