text:
From Complexity.Libs.CookPrelim Require Import Tactics MorePrelim.
From Undecidability.L.Datatypes Require Import Lists LNat LBool LProd LOptions.
From Complexity.NP.SAT Require Import FSAT.

(** * Some generic tools for encoding things as Boolean formulas *)

Section encodings.
  Implicit Types (a : assgn) (v : var).

  (** convenience functions for creating formulas *)
  Notation Ffalse := (¬Ftrue).
  Fixpoint listOr (l : list formula) := match l with
    | [] => Ffalse
    | a :: l => a ∨ listOr l
    end.

  Fixpoint listAnd (l : list formula) := match l with
    | [] => Ftrue
    | a :: l => a ∧ listAnd l
    end.

  Lemma listOr_sat_iff l a : satisfies a (listOr l) <-> exists f, f el l /\ satisfies a f.
  Proof.
    induction l; cbn.
    - unfold satisfies. cbn. split; [congruence | intros (f & [] & _)].
    - unfold satisfies. rewrite evalFormula_or_iff, IHl. split.
      + intros [ H | (f & H1 & H2)]; [exists a0; eauto | exists f; eauto].
      + intros (f & [-> | H1] & H2); [now left | right; exists f; eauto].
  Qed.

  Lemma listAnd_sat_iff l a : satisfies a (listAnd l) <-> forall f, f el l -> satisfies a f.
  Proof.
    induction l; cbn.
    - unfold satisfies. cbn. split; [intros _ f [] | intros _; easy].
    - unfold satisfies. rewrite evalFormula_and_iff, IHl. split.
      + intros (H1 & H2) f [-> | H3%H2]; eauto.
      + intros H; split; [ apply H | intros f H1; apply H]; eauto.
  Qed.

  (** generate the list of values assigned to the variables by a in range [lower, lower + len) *)
  Fixpoint explicitAssignment a lower len :=
    match len with
      | 0 => []
      | S len => explicitAssignment a lower len ++ [list_in_decb Nat.eqb a (lower + len)]
    end.

  Lemma explicitAssignment_length a lower len : |explicitAssignment a lower len| = len.
  Proof.
    revert lower. induction len; intros; cbn.
    - reflexivity.
    - rewrite app_length, IHlen. now cbn.
  Qed.

  Lemma explicitAssignment_nth a lower len k :
     k < len -> nth_error (explicitAssignment a lower len) k = Some (evalVar a (lower + k)).
  Proof.
    intros. induction len.
    - lia.
    - cbn. destruct (le_lt_dec len k).
      + assert (len = k) as <- by lia.
        rewrite nth_error_app2; rewrite explicitAssignment_length; [ rewrite Nat.sub_diag; cbn | lia]. easy.
      + rewrite nth_error_app1; [ | rewrite explicitAssignment_length; easy ]. now apply IHlen.
  Qed.

  Lemma explicitAssignment_app a l1 len1 len2:
    explicitAssignment a l1 (len1 + len2) = explicitAssignment a l1 len1 ++ explicitAssignment a (l1 + len1) len2.
  Proof.
    induction len2; cbn.
    - now rewrite Nat.add_0_r, app_nil_r.
    - rewrite Nat.add_succ_r. cbn. rewrite IHlen2, app_assoc. easy.
  Qed.

  (*from an explicit assignment, we can go back to an assignment *)
  (*s is the variable index at which the explicit assignment is starting *)
  Lemma expAssgn_to_assgn s b :
    {a & forall x, x el a <-> x >= s /\ nth_error b (x - s) = Some true}.
  Proof.
    revert s.
    induction b; cbn; intros.
    - exists []. intros x. destruct (x-s); cbn; easy.
    - destruct (IHb (S s)) as (assgn & IH). destruct a.
      + exists (s :: assgn). intros x. split.
        * intros [-> | H]; [ rewrite Nat.sub_diag; easy | ].
          apply IH in H as (H1 & H2). split; [ lia | ].
          now eapply nth_error_step.
        * intros (H1 & H2). apply le_lt_eq_dec in H1 as [H1 | ->].
          -- right. apply IH. split; [ lia | ]. eapply nth_error_step, H2. lia.
          -- now left.
      + exists assgn. intros x. split.
        * intros (H1 & H2)%IH. split; [ lia | rewrite <- nth_error_step; easy].
        * intros (H1 & H2). apply le_lt_eq_dec in H1 as [H1 | ->].
          -- apply IH. split; [ lia | ]. apply nth_error_step in H2; easy.
          -- rewrite Nat.sub_diag in H2. cbn in H2. congruence.
  Qed.

  Lemma expAssgn_to_assgn_inv a s b : (forall x, x el a <-> x >= s /\ nth_error b (x -s) = Some true)
    -> explicitAssignment a s (|b|) = b.
  Proof.
    intros. apply list_eq_nth_error. split; [ apply explicitAssignment_length | ].
    intros k H1. rewrite explicitAssignment_length in H1.
    rewrite explicitAssignment_nth by apply H1.
    unfold evalVar. destruct list_in_decb eqn:H2.
    - apply list_in_decb_iff in H2; [ | intros; now rewrite Nat.eqb_eq ].
      apply H in H2 as (_ & H2). now replace (s + k - s) with k in H2 by lia.
    - apply list_in_decb_iff' in H2; [ | intros; now rewrite Nat.eqb_eq].
      (*we do a case analysis, thus we do not need XM *)
      destruct (nth_error b k) eqn:H3.
      + destruct b0; [ | easy]. exfalso; apply H2. apply H.
        now replace (s + k - s) with k by lia.
      + apply nth_error_None in H3. lia.
  Qed.

  (*we define what it means for a formula to encode a predicate *)
  Definition predicate := list bool -> Prop.
  Implicit Type (p : predicate).
  Definition encodesPredicateAt (start : nat) (l : nat) f p:= forall a, satisfies a f <-> p (explicitAssignment a start l).

  (*given an explicitAssignment, we can project out a range of variables, given by [start, start+len) *)
  Definition projVars start len (l : list bool) := firstn len (skipn start l).

  Lemma projVars_length l s m : |l| >= (s + m) -> |projVars s m l| = m.
  Proof.
    intros. unfold projVars. rewrite firstn_length. rewrite skipn_length. lia.
  Qed.

  Lemma projVars_app1 l1 l2 m : |l1| = m -> projVars 0 m (l1 ++ l2) = l1.
  Proof.
    intros. unfold projVars. cbn. rewrite firstn_app. subst.
    now rewrite Nat.sub_diag, firstn_O, app_nil_r, firstn_all.
  Qed.

  Lemma projVars_app2 l1 l2 u m : |l1| = u -> projVars u m (l1 ++ l2) = projVars 0 m l2.
  Proof.
    intros. unfold projVars. rewrite skipn_app; [ | easy]. now cbn.
  Qed.

  Lemma projVars_app3 l1 l2 u1 u2 m : |l1| = u1 -> projVars (u1 + u2) m (l1 ++ l2) = projVars u2 m l2.
  Proof.
    intros. unfold projVars. erewrite skipn_add; [ easy| lia].
  Qed.

  Lemma projVars_all l m : m = |l| -> projVars 0 m l = l.
  Proof.
    intros. unfold projVars. cbn. rewrite H. apply firstn_all.
  Qed.

  Lemma projVars_comp l1 l2 len1 len2 m: projVars l1 len1 (projVars l2 len2 m) = projVars (l1 + l2) (min len1 (len2 - l1)) m.
  Proof.
    unfold projVars. intros.
    rewrite skipn_firstn_skipn. rewrite firstn_firstn. reflexivity.
  Qed.

  Lemma projVars_add s l1 l2 m : projVars s (l1 + l2) m = projVars s l1 m ++ projVars (s + l1) l2 m.
  Proof.
    unfold projVars. rewrite firstn_add, skipn_skipn. now rewrite Nat.add_comm.
  Qed.

  Lemma projVars_length_le start l m: |projVars start l m| <= |m|.
  Proof.
    unfold projVars.
    rewrite firstn_length. rewrite skipn_length. lia.
  Qed.

  Lemma projVars_length_le2 start l m : |projVars start l m| <= l.
  Proof.
    unfold projVars. rewrite firstn_length, skipn_length. lia.
  Qed.

  Lemma projVars_in_ge start l m : start <= |m| -> projVars start (|l|) m = l -> |m| >= start + |l|.
  Proof.
    intros H0 H. unfold projVars in H. rewrite <- H, firstn_length, skipn_length. lia.
  Qed.

  (*encodings of two predicates can be combined*)
  Definition combinedLength start1 start2 l1 l2 := max (start1 +l1) (start2 + l2) - min start1 start2.
  Definition combinedStart start1 start2 := min start1 start2.

  (** from the combined assignment for the combination of two formulas, we can restore an assignment for the first formula *)
  Lemma projVars_combined1 s1 s2 l1 l2 a: explicitAssignment a s1 l1 =
    projVars (s1 - combinedStart s1 s2) l1 (explicitAssignment a (combinedStart s1 s2) (combinedLength s1 s2 l1 l2)).
  Proof.
    unfold projVars.
    apply list_eq_nth_error. split.
    - rewrite explicitAssignment_length. unfold combinedStart, combinedLength. rewrite firstn_length.
      rewrite skipn_length. rewrite explicitAssignment_length. lia.
    - intros. rewrite explicitAssignment_length in H. unfold combinedStart, combinedLength.
      rewrite nth_error_firstn; [ | apply H].
      rewrite nth_error_skipn. rewrite !explicitAssignment_nth; [easy | lia | lia].
  Qed.

  (*...and for the second *)
  Lemma projVars_combined2 s1 s2 l1 l2 a: explicitAssignment a s2 l2 =
    projVars (s2 - combinedStart s1 s2) l2 (explicitAssignment a (combinedStart s1 s2) (combinedLength s1 s2 l1 l2)).
  Proof.
    unfold combinedStart, combinedLength. rewrite Nat.min_comm. rewrite Nat.max_comm. apply projVars_combined1.
  Qed.

  (*two formulae can be combined via ∧ *)
  Lemma encodesPredicate_and start1 start2 l1 l2 f1 f2 p1 p2 :
    encodesPredicateAt start1 l1 f1 p1 -> encodesPredicateAt start2 l2 f2 p2
    -> encodesPredicateAt (combinedStart start1 start2) (combinedLength start1 start2 l1 l2) (f1 ∧ f2)
        (fun m => (p1 (projVars (start1 - combinedStart start1 start2) l1 m)
            /\ p2 (projVars (start2 - combinedStart start1 start2) l2 m))).
  Proof.
    intros G1 G2.
    intros a. split; intros H.
    + apply evalFormula_and_iff in H as (H1 & H2).
      rewrite <- projVars_combined1, <- projVars_combined2.
      unfold encodesPredicateAt in G1, G2. rewrite <- G1, <- G2. easy.
    + rewrite <- projVars_combined1, <- projVars_combined2 in H.
      unfold satisfies. apply evalFormula_and_iff.
      split; [apply G1, H | apply G2, H].
  Qed.

  (*...and with ∨*)
  Lemma encodesPredicate_or start1 start2 l1 l2 f1 f2 p1 p2 :
    encodesPredicateAt start1 l1 f1 p1 -> encodesPredicateAt start2 l2 f2 p2
    -> encodesPredicateAt (combinedStart start1 start2) (combinedLength start1 start2 l1 l2) (f1 ∨ f2)
        (fun m => (p1 (projVars (start1 - combinedStart start1 start2) l1 m)
            \/ p2 (projVars (start2 - combinedStart start1 start2) l2 m))).
  Proof.
    intros G1 G2.
    intros a. split; intros H.
    + apply evalFormula_or_iff in H as [H | H];
      rewrite <- projVars_combined1, <- projVars_combined2;
      unfold encodesPredicateAt in G1, G2; rewrite <- G1, <- G2; easy.
    + rewrite <- projVars_combined1, <- projVars_combined2 in H.
      unfold satisfies. apply evalFormula_or_iff.
      destruct H as [H | H]; [left; apply G1, H | right; apply G2, H].
  Qed.

  (** next, we do the same for lists of formulas where the individual formulas are placed in a regular pattern starting at an index s with an offset step *)
  Fixpoint tabulate_step (step s n : nat) :=
    match n with
      | 0 => []
      | S n => s :: tabulate_step step (step + s) n
    end.
  Definition tabulate_formula s step n (t : nat -> formula) := map t (tabulate_step step s n).

  Lemma in_tabulate_step_iff step s n x : x el tabulate_step step s n <-> exists i, i < n /\ x = s + step * i.
  Proof.
    revert s. induction n; cbn; intros.
    - split; [easy | intros (i & H & _); lia ].
    - split.
      + intros [-> | H%IHn]; [exists 0; lia | ].
        destruct H as (i & H1 & ->). exists (S i). lia.
      + intros (i & H1 & H2).
        destruct i.
        * now left.
        * right. apply IHn. exists i. lia.
  Qed.

  Lemma in_tabulate_formula_iff s step n t f:
    f el tabulate_formula s step n t <-> exists i, i < n /\ f = t (s + step * i).
  Proof.
    unfold tabulate_formula. rewrite in_map_iff. setoid_rewrite in_tabulate_step_iff.
    split.
    - intros (x & <- & (i & H1 & ->)). exists i. eauto.
    - intros (i & H1 & ->). exists (s + step * i). eauto.
  Qed.

  Fact projVars_mul_offset a s step i l n: i < n -> explicitAssignment a (s + step * i) l = projVars (step * i) l (explicitAssignment a s (step * n + (l - step))).
  Proof.
    intros H. apply list_eq_nth_error.
    split.
    - rewrite projVars_length; rewrite !explicitAssignment_length; [lia | ]. nia.
    - rewrite explicitAssignment_length. intros k H1.
      unfold projVars. rewrite nth_error_firstn by apply H1.
      rewrite nth_error_skipn. rewrite !explicitAssignment_nth.
      + easy.
      + nia.
      + apply H1.
  Qed.

  Lemma encodesPredicate_listOr_tabulate l (t : nat -> formula) p :
    (forall s, encodesPredicateAt s l (t s) p)
    -> forall s step n, encodesPredicateAt s (step * n + (l - step)) (listOr (tabulate_formula s step n t))
        (fun m => exists i, i < n /\ p (projVars (step * i) l m)).
  Proof.
    (* we have to add l - step for the case that l > step; this is the case when creating the rewrite windows, for instance *)
    intros H s step n. unfold encodesPredicateAt. intros a.
    rewrite listOr_sat_iff. setoid_rewrite in_tabulate_formula_iff.
    split.
    - intros (f & (i & H1 & ->) & H2). exists i. split; [easy | ].
      specialize (H (s + step * i)). apply H in H2.
      rewrite <- projVars_mul_offset by apply H1. apply H2.
    - intros (i & H1 & H2). exists (t (s + step * i)). split.
      + exists i. eauto.
      + apply H. erewrite projVars_mul_offset by apply H1. apply H2.
  Qed.

  Lemma encodesPredicate_listAnd_tabulate l (t : nat -> formula) p :
    (forall s, encodesPredicateAt s l (t s) p)
    -> forall s step n, encodesPredicateAt s (step * n + (l - step)) (listAnd (tabulate_formula s step n t))
        (fun m => forall i, i < n -> p (projVars (step * i) l m)).
  Proof.
    intros H s step n. unfold encodesPredicateAt. intros a.
    rewrite listAnd_sat_iff. setoid_rewrite in_tabulate_formula_iff.
    split.
    - intros H1 i H2. rewrite <- projVars_mul_offset by apply H2.
      apply H, H1. exists i; eauto.
    - intros H1 f (i & H2 & ->). apply H.
      erewrite projVars_mul_offset by apply H2. now apply H1.
  Qed.

  (** similarly, we can combine multiple formulas at the same position *)
  Lemma encodesPredicate_listOr_map (X : Type) s l (es : list X) (p : X -> predicate) (f : X -> formula) :
    (forall e, e el es -> encodesPredicateAt s l (f e) (p e))
    -> encodesPredicateAt s l (listOr (map f es)) (fun m => exists e, e el es /\ p e m).
  Proof.
    intros H. unfold encodesPredicateAt. intros a.
    rewrite listOr_sat_iff. setoid_rewrite in_map_iff.
    split.
    - intros (fo & (x & <- & Hel) & H1). apply (H _ Hel) in H1. eauto.
    - intros (x & Hel & H1). apply (H _ Hel) in H1. exists (f x).
      split; eauto.
  Qed.

  Lemma encodesPredicate_listAnd_map (X : Type) s l (es : list X) (p : X -> predicate) (f : X -> formula) :
    (forall e, e el es -> encodesPredicateAt s l (f e) (p e))
    -> encodesPredicateAt s l (listAnd (map f es)) (fun m => forall e, e el es -> p e m).
  Proof.
    intros H. unfold encodesPredicateAt. intros a.
    rewrite listAnd_sat_iff. setoid_rewrite in_map_iff.
    split.
    - intros H1 e Hel. apply (H _ Hel). apply H1. eauto.
    - intros H1 fo (x & <- & Hel). apply (H _ Hel). now apply H1.
  Qed.

  (*encoding of single literals *)
  Definition encodeLiteral (v : var) (sign : bool) : formula := if sign then v else ¬ v.

  Lemma encodeLiteral_correct v sign : forall a, satisfies a (encodeLiteral v sign) <-> evalVar a v = sign.
  Proof.
    intros. unfold satisfies, encodeLiteral. destruct sign; cbn; [ tauto |simp_bool; tauto ].
  Qed.

  Lemma encodeLiteral_encodesPredicate v sign : encodesPredicateAt v 1 (encodeLiteral v sign) (fun l => l = [sign]).
  Proof.
    intros. split; intros.
    + apply encodeLiteral_correct in H. specialize (explicitAssignment_length a v 1) as H1.
      assert (0 < 1) as H2 by lia.
      specialize (@explicitAssignment_nth a v 1 0 H2) as H3.
      destruct explicitAssignment as [ | s l]; cbn in H1; [ congruence | destruct l; [ | cbn in H1; congruence]].
      cbn in H3. now inv H3.
    + apply encodeLiteral_correct. assert (0 < 1) as H2 by lia.
      specialize (@explicitAssignment_nth a v 1 0 H2) as H1.
      rewrite H in H1; cbn in H1. now inv H1.
  Qed.

  (*for predicates which are equivalent, encoding is equivalent *)
  Lemma encodesPredicateAt_extensional s l f p1 p2 : (forall m, |m| = l -> p1 m <-> p2 m)
      -> encodesPredicateAt s l f p1 <-> encodesPredicateAt s l f p2.
  Proof.
    intros. unfold encodesPredicateAt. split; intros; specialize (H (explicitAssignment a s l) (explicitAssignment_length _ _ _)); [now rewrite <- H | now rewrite H].
  Qed.

  (*a procedure that tries to simplify parts of the terms introduced by the combination lemmas for ∧ and ∨ *)
  Ltac encodesPredicateAt_comp_simp H :=
    unfold combinedStart, combinedLength in H;
    try (rewrite Nat.min_l in H by nia); try (rewrite Nat.min_r in H by nia);
    try (rewrite Nat.max_l in H by nia); try (rewrite Nat.max_r in H by nia);
    try rewrite !Nat.sub_diag in H.

  (*encoding of lists *)
  Fixpoint encodeListAt (startA : nat) (l : list bool) :=
    match l with
    | [] => Ftrue
    | x :: l => (encodeLiteral startA x) ∧ (encodeListAt (1 + startA) l)
    end.

  Lemma encodeListAt_encodesPredicate start l : encodesPredicateAt start (|l|) (encodeListAt start l) (fun m => m = l).
  Proof.
    revert start. induction l; intros.
    - cbn. split; [eauto | ]. unfold satisfies. intros; easy.
    - cbn. specialize (@encodesPredicate_and start (S start) 1 (|l|) (encodeLiteral start a) (encodeListAt (S start) l) _ _ (encodeLiteral_encodesPredicate start a) (IHl (S start))) as H1.
      encodesPredicateAt_comp_simp H1.
      replace (S start - start) with 1 in H1 by lia.
      replace (S start + (|l|) - start) with (S (|l|)) in H1 by lia.
      eapply encodesPredicateAt_extensional; [ | apply H1].
      intros m H0. unfold projVars.
      destruct m; cbn; [split; intros; easy | ].
      split.
      + intros H. inv H. now rewrite firstn_all.
      + intros (H2 & H3). inv H2. f_equal. apply Nat.succ_inj in H0. now apply firstn_all_inv.
  Qed.
End encodings.
Ltac encodesPredicateAt_comp_simp H :=
  unfold combinedStart, combinedLength in H;
  try (rewrite Nat.min_l in H by nia); try (rewrite Nat.min_r in H by nia);
  try (rewrite Nat.max_l in H by nia); try (rewrite Nat.max_r in H by nia);
  try rewrite !Nat.sub_diag in H.

(** *** extraction *)
From Undecidability.L.Tactics Require Import LTactics GenEncode.
From Complexity.Libs.CookPrelim Require Import PolyBounds.
From Undecidability.L.Datatypes Require Import LProd LOptions LBool LSum.
From Undecidability.L.Functions Require Import EqBool.

Implicit Type (p : nat -> Prop).

(** listAnd *)
Definition c__listAnd := 12.
Definition listAnd_time (l : list formula) := (|l| + 1) * c__listAnd.
#[export]
Instance term_listAnd : computableTime' listAnd (fun l _ => (listAnd_time l, tt)).
Proof.
  extract. solverec. all: unfold listAnd_time, c__listAnd; solverec.
Qed.

Lemma listAnd_varsIn (p : nat ->Prop) l: (forall f, f el l -> formula_varsIn p f) -> formula_varsIn p (listAnd l).
Proof.
  unfold formula_varsIn. intros H; induction l; cbn.
  - intros v H1. inv H1.
  - intros v H1. inv H1; [eapply H; eauto | eapply IHl; eauto].
Qed.

Lemma listAnd_size l : formula_size (listAnd l) <= sumn (map formula_size l) + |l| + 1.
Proof.
  induction l; cbn; [lia | rewrite IHl; lia].
Qed.

(** listOr *)
Definition c__listOr := 12.
Definition listOr_time (l : list formula) := (|l| + 1) * c__listOr.
#[export]
Instance term_listOr : computableTime' listOr (fun l _ => (listOr_time l, tt)).
Proof.
  extract. solverec. all: unfold listOr_time, c__listOr; solverec.
Qed.

Lemma listOr_varsIn p l: (forall f, f el l -> formula_varsIn p f) -> formula_varsIn p (listOr l).
Proof.
  unfold formula_varsIn. intros H; induction l; cbn.
  - intros v H1. inv H1. inv H2.
  - intros v H1. inv H1; [eapply H; eauto | eapply IHl; eauto].
Qed.

Lemma listOr_size l : formula_size (listOr l) <= sumn (map formula_size l) + |l| + 2.
Proof.
  induction l; cbn; [lia | rewrite IHl; lia].
Qed.

(** tabulate_step *)
Definition c__tabulateStep := 13 + c__add1.
Definition tabulate_step_time (step n : nat) := n * (add_time step + c__tabulateStep) + c__tabulateStep.
#[export]
Instance term_tabulate_step : computableTime' tabulate_step (fun step _ => (5, fun s _ => (1, fun n _ => (tabulate_step_time step n, tt)))).
Proof.
  extract. solverec.
  all: unfold tabulate_step_time, c__tabulateStep; solverec.
Qed.

Definition poly__tabulateStep n := n * ((n + 1) * c__add + c__tabulateStep) + c__tabulateStep.
Lemma tabulate_step_time_bound step n : tabulate_step_time step n <= poly__tabulateStep (size (enc step) + size (enc n)).
Proof.
  unfold tabulate_step_time. rewrite size_nat_enc_r with (n := n) at 1.
  unfold add_time. rewrite size_nat_enc_r with (n := step) at 1.
  unfold poly__tabulateStep; solverec.
Qed.
Lemma tabulate_step_poly : monotonic poly__tabulateStep /\ inOPoly poly__tabulateStep.
Proof.
  unfold poly__tabulateStep; split; smpl_inO.
Qed.

Lemma tabulate_step_length step s n: |tabulate_step step s n| = n.
Proof.
  revert step s. induction n; cbn; intros; [lia | rewrite IHn; lia].
Qed.

(** tabulate_formula *)
Definition c__tabulateFormula := 8.
Definition tabulate_formula_time (s step n : nat) (tf : nat -> nat) := tabulate_step_time step n + map_time tf (tabulate_step step s n) + c__tabulateFormula.
#[export]
Instance term_tabulate_formula : computableTime' tabulate_formula (fun s _ => (1, fun step _ => (1, fun n _ => (1, fun t tf => (tabulate_formula_time s step n (callTime tf), tt))))).
Proof.
  extract. solverec.
  unfold tabulate_formula_time, c__tabulateFormula; solverec.
Qed.

Lemma formula_varsIn_monotonic (p1 p2 : nat -> Prop) : (forall n, p1 n -> p2 n) -> forall f, formula_varsIn p1 f -> formula_varsIn p2 f.
Proof.
  intros H f. unfold formula_varsIn. eauto.
Qed.

Lemma tabulate_formula_varsIn s step n t (g : nat -> nat):
  (forall start, formula_varsIn (fun n => n < g start) (t start))
  -> monotonic g
  -> forall f, f el tabulate_formula s step n t -> formula_varsIn (fun v => v < g (s + step * (n -1))) f.
Proof.
  intros H H0 f Hel. unfold tabulate_formula in Hel. apply in_map_iff in Hel as (i & <- & Hel).
  apply in_tabulate_step_iff in Hel as (i' & H1 & ->).
  eapply formula_varsIn_monotonic.
  2: apply H.
  cbn. intros n' Hn'. unfold monotonic in H0. specialize (H0 (s + step * i') (s + step * (n -1)) ltac:(nia)). nia.
Qed.

Lemma tabulate_formula_length s step n t : |tabulate_formula s step n t| = n.
Proof.
  revert s step. induction n; cbn; intros; [lia | ].
  unfold tabulate_formula in IHn. now rewrite IHn.
Qed.

(** encodeLiteral *)
Definition c__encodeLiteral := 6.
#[export]
Instance term_encodeLiteral : computableTime' encodeLiteral (fun n _ => (1, fun b _ => (c__encodeLiteral, tt))).
Proof.
  extract. solverec. all: unfold c__encodeLiteral; solverec.
Qed.

Lemma encodeLiteral_size v b : formula_size (encodeLiteral v b) <= 2.
Proof.
  unfold encodeLiteral. destruct b; cbn; lia.
Qed.

Ltac varsIn_inv :=
  repeat match goal with
    | [ H: formula_varsIn ?f |- _] => inv H
    | [ H: varInFormula ?v ?f|- _]=> inv H
  end.

Lemma encodeLiteral_varsIn v b : formula_varsIn (fun n => n = v) (encodeLiteral v b).
Proof.
  unfold encodeLiteral. destruct b; cbn; intros v' H; varsIn_inv; lia.
Qed.

(** encodeListAt *)
Definition c__encodeListAt := c__encodeLiteral + c__add1 + add_time 1 + 15.
Definition encodeListAt_time (l : list bool) := (|l| + 1) * c__encodeListAt.
#[export]
Instance term_encodeListAt : computableTime' encodeListAt (fun s _ => (5, fun l _ => (encodeListAt_time l, tt))).
Proof.
  extract. solverec.
  all: unfold encodeListAt_time, c__encodeListAt; solverec.
Qed.

Definition poly__encodeListAt n := (n + 1) * c__encodeListAt.
Lemma encodeListAt_time_bound l : encodeListAt_time l <= poly__encodeListAt (size (enc l)).
Proof.
  unfold encodeListAt_time. rewrite list_size_length.
  unfold poly__encodeListAt; solverec.
Qed.
Lemma encodeListAt_poly : monotonic poly__encodeListAt /\ inOPoly poly__encodeListAt.
Proof.
  unfold poly__encodeListAt; split; smpl_inO.
Qed.

Lemma encodeListAt_varsIn start l: formula_varsIn (fun n => n >= start /\ n < start + |l|) (encodeListAt start l).
Proof.
  revert start; induction l; cbn; intros.
  - intros v H; varsIn_inv.
  - intros v H. inv H.
    + apply encodeLiteral_varsIn in H1. lia.
    + apply IHl in H1. lia.
Qed.

Lemma encodeListAt_size start l : formula_size (encodeListAt start l) <= 3 * (|l|) + 1.
Proof.
  revert start; induction l; cbn -[Nat.mul]; intros; [lia | rewrite IHl]. rewrite encodeLiteral_size. lia.
Qed.

author: uds-psl

repo: coq-library-complexity


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.solinas32_2e384m317_17limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition sub :
  { sub : feBW_tight -> feBW_tight -> feBW_loose
  | forall a b, phiBW_loose (sub a b) = F.sub (phiBW_tight a) (phiBW_tight b) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_sub ().
  Show Ltac Profile.
Time Defined.

Print Assumptions sub.


text:
(*
 * Copyright (c) 2017-present,
 * Programming Research Laboratory (ROPAS), Seoul National University, Korea
 * This software is distributed under the term of the BSD-3 clause license.
 *)
(** * Densification function (Sen -- SenLocal) *)

Set Implicit Arguments.

Require Import vgtac.
Require Import UserProofType Syn.
Require Import Global SemCommon.
Require DomSen SemSenLocal.

Module Make (Import PInput : PINPUT).

Local Open Scope type.

Module Sen := DomSen.Make PInput.

Module SenLocal := SemSenLocal.Make PInput.

Section Pgm.

Variable g : G.t.

Let pgm : InterCfg.t := G.icfg g.

Variable amap : access_map.

Fixpoint densify_mem senl_t callee calls : Mem.t :=
  match calls with
    | nil => Mem.bot
    | cons calln tl =>
      let access := get_all_access callee amap in
      let call_m := senl_t (calln, Outputof, tl) in
      let densified := Mem.subtract access call_m in
      Mem.join densified (densify_mem senl_t (InterNode.get_pid calln) tl)
  end.

Definition densify_state (senl_t : Sen.state_t) : Sen.state_t :=
  fun idx =>
    let '(node, mempos, calls) := idx in
    Mem.join (senl_t idx)
             (densify_mem senl_t (InterNode.get_pid node) calls).

End Pgm.

Local Close Scope type.

End Make.

author: ropas

repo: zooberry

save_path: github-repos/coq/ropas-zooberry


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.montgomery32_2e383m187_12limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition add :
  { add : feBW_small -> feBW_small -> feBW_small
  | forall a b, phiM_small (add a b) = F.add (phiM_small a) (phiM_small b) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_add ().
  Show Ltac Profile.
Time Defined.

Print Assumptions add.


text:
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.RealInfix.

Parameter pow2: Z -> R.

Axiom Power_0 : ((pow2 0%Z) = 1%R).

Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
  ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R).

Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z ->
  ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R).

Axiom Power_s_all : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R).

Axiom Power_p_all : forall (n:Z),
  ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R).

Axiom Power_1_2 : ((05 / 10)%R = (1%R / 2%R)%R).

Axiom Power_1 : ((pow2 1%Z) = 2%R).

Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R).

Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 2; admit.

(* Why3 goal *)
Theorem Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z ->
  ~ ((pow2 n) = 0%R).
(* Why3 intros n h1. *)
intros n Hn.
generalize Hn.
pattern n; apply Z_lt_induction; auto.
ae.
Admitted.

author: florianschanda