text:
Set Implicit Arguments.

Require Export natDedGram.
Require Export struct_ex.
Require Export tacticsDed.
Require Export unbounDep.

(* in this example, we analyze unbounded dependencies phenomena *)

Inductive I:Set:=m1.
Inductive J:Set:= m2.
Inductive A:Set:=|np|s|n.

Definition eqdecI:eqdec I.
solve_eqdec.
Defined.

Definition eqdecJ:eqdec J.
solve_eqdec.
Defined.

Definition eqdecA:eqdec A.
solve_eqdec.
Defined.

Notation "'!' F":=(At (I:=I) (J:=J) F)(at level 40).
Notation "A '/1' B"
 := (Slash m1 A B) (at level 41,  right associativity) .

Notation " A '\1' B"
 := (Backslash m1 A B) (at level 41,  right associativity).

Notation " A 'o1' B"
 := (Dot m1 A B) (at level 38, left associativity) .

Notation "T1 ,1 T2" :=
(Comma m1 T1 T2)(at level 45, right associativity).

Notation "A ;1 B":=
(comW m1 A B)(at level 42, right associativity).

Notation "'[]0' A" :=(Box m2 A) (at level 30).
Notation "'<>0' A":=(Diamond m2 A)(at level 30).
Notation "'#' w":=(oneW I J w)(at level 40).

Notation "h :> ty":=(res h ty)(at level 35).

(* terminals*)
Inductive W:Set:=|whom|Mary|thinks|Peter|likes.
Definition lex(w:W):list (Form I J  A ):=
match w with
|whom=>((!n\1 !n)/1 (!s /1 <>0 []0 !np))::nil
|Mary=> !np ::nil
|thinks=>((!np\1 !s)/1 !s)::nil
|Peter=> !np::nil
|likes=> ((!np \1 !s)/1 !np) ::nil
end.
Definition lex1:synLexicon.
esplit.
eexact eqdecI.
eexact eqdecJ.
eexact eqdecA.
eexact lex.
Defined.

Definition ext1:=(MA2Diam m1 m2) U NL.
(* definition of the grammar *)
Definition gram1:synGram:=mk_gramS lex1 ext1.

(* definition of the fragment to be derived *)
Definition my_fragment:=whom::Mary::thinks::Peter::likes::nil.

Definition my_contextW:=
#whom ;1 #Mary ;1 #thinks ;1 #Peter ;1 #likes.

Definition treeDeriv:||gram1||: my_fragment>>(!n \1 !n).
setCont0 my_contextW.
simpl.
eslashE.
axiom.
apply SlashI with 0.
apply unboundDep with 1.
inExt.
simpl.
ebackE.
constructor.
eslashE.
constructor.
ebackE.
constructor.
eslashE.
constructor.
apply BoxE;constructor.
Defined.

author: coq-contribs

repo: icharate

save_path: github-repos/coq/coq-contribs-icharate


text:
From Hammer Require Import Hammer.

Set Implicit Arguments.
Unset Standard Proposition Elimination Names.

Require Export List.

Require Import Program Omega Factorial.
Require Import Bool Morphisms Relations RelationClasses Permutation.
From QuicksortComplexity Require Import util.

Hint Resolve
in_map Permutation_refl.

Hint Constructors NoDup.

Hint Constructors
NoDup Permutation.

Arguments length {A}.
Arguments Permutation {A}.
Arguments map {A B}.
Arguments tail {A}.

Section count.

Context {X: Type} (p: X -> bool).

Fixpoint count (l: list X): nat :=
match l with
| nil => 0
| h :: t => if p h then S (count t) else count t
end.

Lemma count_app l l': count (l ++ l') = count l + count l'.
Proof with auto. hammer_hook "list_utils" "list_utils.count_app".
induction l...
simpl.
destruct (p a)...
intros.
rewrite IHl...
Qed.

Lemma count_0 l: (forall x, In x l -> p x = false) -> count l = 0.
Proof with auto. hammer_hook "list_utils" "list_utils.count_0". induction l... simpl. intros. rewrite H... Qed.

Lemma count_le l: count l <= length l.
Proof with auto with arith. hammer_hook "list_utils" "list_utils.count_le".
induction l...
simpl.
destruct (p a)...
Qed.

Lemma count_filter_le (f: X -> bool) x: count (filter f x) <= count x.
Proof with auto with arith. hammer_hook "list_utils" "list_utils.count_filter_le".
induction x...
simpl.
destruct (f a).
simpl.
destruct (p a)...
destruct (p a)...
Qed.

Hint Resolve count_le.

Lemma count_lt v l: In v l -> p v = false -> count l < length l.
Proof with auto with arith. hammer_hook "list_utils" "list_utils.count_lt".
induction l; simpl; intros.
elimtype False...
inversion_clear H.
subst.
rewrite H0...
destruct (p a)...
Qed.

End count.

Hint Resolve @count_le.

Lemma NoDup_map_inv' A B (f: A -> B) (l: list A): NoDup (map f l) -> NoDup l.
Proof with auto. hammer_hook "list_utils" "list_utils.NoDup_map_inv'".
induction l...
simpl.
intros.
inversion_clear H.
apply NoDup_cons...
Qed.

Lemma length_filter X (p: X -> bool) (l: list X): length (filter p l) = count p l.
Proof with auto. hammer_hook "list_utils" "list_utils.length_filter". intros. induction l... simpl. destruct (p a)... simpl... Qed.

Lemma length_filter_le T (p: T -> bool) (l: list T): length (filter p l) <= length l.
Proof. hammer_hook "list_utils" "list_utils.length_filter_le". intros. rewrite length_filter. apply count_le. Qed.

Lemma filter_all X (p: X -> bool) (l: list X):
(forall x, In x l -> p x = true) -> filter p l = l.
Proof with auto. hammer_hook "list_utils" "list_utils.filter_all".
induction l...
simpl.
intros.
rewrite H...
rewrite IHl...
Qed.

Lemma In_filter T (p: T -> bool) (t: T): p t = true -> forall l, In t l -> In t (filter p l).
Proof. hammer_hook "list_utils" "list_utils.In_filter". intros. destruct (filter_In p t l). apply H2; auto. Qed.

Lemma incl_filter X (p: X -> bool) (l: list X): incl (filter p l) l.
Proof with auto. hammer_hook "list_utils" "list_utils.incl_filter".
unfold incl.
induction l; simpl...
intros.
destruct (p a); firstorder.
Qed.

Lemma incl_trans A (x y: list A): incl x y -> forall z, incl y z -> incl x z.
Proof. hammer_hook "list_utils" "list_utils.incl_trans". do 5 intro. apply H0. apply H. assumption. Qed.

Hint Resolve incl_filter.

Lemma filter_preserves_incl X (p: X -> bool) (a b: list X): incl a b -> incl (filter p a) (filter p b).
Proof with auto. hammer_hook "list_utils" "list_utils.filter_preserves_incl".
unfold incl.
intros.
destruct (filter_In p a0 a).
clear H2.
destruct (H1 H0).
clear H1.
apply In_filter...
Qed.

Hint Resolve filter_preserves_incl.

Lemma In_inv_perm X (x: X) (l: list X):
In x l -> exists l', Permutation (x :: l') l.
Proof with eauto. hammer_hook "list_utils" "list_utils.In_inv_perm".
induction l; intros; inversion_clear H. subst...
destruct IHl...
Qed.

Lemma In_map_inv T U (f: T -> U) (l: list T) (y: U): In y (map f l) -> exists x, f x = y /\ In x l.
Proof. hammer_hook "list_utils" "list_utils.In_map_inv". induction l; firstorder. Qed.

Arguments In_map_inv [T U f l y].

Instance In_Permutation A (x: A): Proper (Permutation ==> iff) (In x).
Proof. hammer_hook "list_utils" "list_utils.In_Permutation".
repeat intro.
pose proof (Permutation_in).
pose proof (Permutation_sym).
firstorder.
Qed.

Instance Permutation_NoDup {X}: Proper (Permutation ==> iff) (@NoDup X).
Proof with firstorder auto. hammer_hook "list_utils" "list_utils.Permutation_NoDup".
pose proof NoDup_cons.
intros ? ? E.
induction E; [firstorder | | | firstorder].
split; intro A; inversion_clear A; apply NoDup_cons...
rewrite <- E...
rewrite E...
split; intro A; inversion_clear A; inversion_clear H1...
Qed.

Hint Resolve incl_tran.

Lemma Permutation_incl X (a b: list X): Permutation a b -> incl a b.
Proof. hammer_hook "list_utils" "list_utils.Permutation_incl". induction 1; firstorder. Qed.

Instance count_perm A: Proper (pointwise_relation _ eq ==> Permutation ==> eq) (@count A).
Proof with auto. hammer_hook "list_utils" "list_utils.count_perm".
intros p p' E.
assert (forall l, count p l = count p' l).
induction l...
simpl. rewrite E, IHl...
intros l l' P.
induction P; intros; simpl...
rewrite IHP.
rewrite E...
repeat rewrite E.
destruct (p' y); destruct (p' x)...
rewrite IHP1.
rewrite <- H...
Qed.

Lemma pointwise_eq_refl A B (x: A -> B): pointwise_relation A eq x x.
Proof. hammer_hook "list_utils" "list_utils.pointwise_eq_refl". reflexivity. Qed.
Hint Immediate pointwise_eq_refl.

Instance count_perm_simple A (p: A -> bool): Proper (Permutation ==> eq) (count p).
Proof. hammer_hook "list_utils" "list_utils.count_perm_simple". intros. apply count_perm. auto. Qed.

Instance filter_eq_morphism T: Proper (pointwise_relation _ eq ==> eq ==> eq) (@filter T).
Proof with auto. hammer_hook "list_utils" "list_utils.filter_eq_morphism".
repeat intro.
subst.
induction y0...
simpl.
rewrite H.
rewrite IHy0...
Qed.

Instance filter_perm X: Proper (pointwise_relation _ eq ==> Permutation ==> Permutation) (@filter X).
Proof with auto. hammer_hook "list_utils" "list_utils.filter_perm".
repeat intro.
induction H0; rewrite H in *; simpl...
destruct (y x0)...
destruct (y y0); destruct (y x0)...
eauto.
Qed.

Lemma complementary_filter_perm A (p: A -> bool) (l: list A):
Permutation l (filter p l ++ filter (negb ∘ p) l).
Proof with auto. hammer_hook "list_utils" "list_utils.complementary_filter_perm".
induction l...
simpl.
unfold compose.
destruct (p a); simpl...
apply Permutation_cons_app...
Qed.

Lemma filter_none X (p: X -> bool) (l: list X): (forall x, In x l -> p x = false) <-> filter p l = nil.
Proof with auto. hammer_hook "list_utils" "list_utils.filter_none".
induction l.
split...
intros.
inversion H0.
destruct IHl.
split; simpl; intros.
rewrite H1...
destruct H2.
subst.
destruct (p x)...
discriminate.
apply H0...
destruct (p a)...
discriminate.
Qed.

Lemma incl_map X Y (f: X -> Y) (a b: list X): incl a b -> incl (map f a) (map f b).
Proof with auto. hammer_hook "list_utils" "list_utils.incl_map".
do 3 intro.
destruct (In_map_inv H0).
destruct H1.
subst...
Qed.

Lemma incl_in T (a b: list T): incl a b -> forall x, In x a -> In x b.
Proof. hammer_hook "list_utils" "list_utils.incl_in". auto. Qed.

Lemma incl_In X (x: X) (l: list X): In x l -> forall l', incl l l' -> In x l'.
Proof. hammer_hook "list_utils" "list_utils.incl_In". intros. apply H0. assumption. Qed.

Lemma NoDup_filter T (p: T -> bool) (l: list T):
NoDup l -> NoDup (filter p l).
Proof with auto. hammer_hook "list_utils" "list_utils.NoDup_filter".
induction l...
simpl.
intros.
inversion_clear H.
destruct (p a)...
apply NoDup_cons...
intro.
apply H0...
apply (incl_filter p l)...
Qed.

Lemma length_excl_counts X (p: X -> bool) (l: list X):
length l = count p l + count (negb ∘ p) l.
Proof with auto. hammer_hook "list_utils" "list_utils.length_excl_counts".
unfold compose.
induction l...
intros.
simpl.
rewrite IHl.
destruct (p a); simpl...
Qed.

Lemma count_filtered X (p q: X -> bool):
(forall x, q x = true -> p x = false) ->
forall l, count p (filter q l) = 0.
Proof with auto. hammer_hook "list_utils" "list_utils.count_filtered".
induction l...
simpl.
cset (H a).
destruct (q a)...
simpl.
rewrite H0...
Qed.

Lemma app_nil_r T (l: list T): l ++ nil = l.
Proof with auto. hammer_hook "list_utils" "list_utils.app_nil_r". induction l... simpl. rewrite IHl... Qed.

Hint Resolve Permutation_map.

Lemma map_cons T U (f: T -> U) (h: T) (l: list T): map f (h :: l) = f h :: map f l.
Proof. hammer_hook "list_utils" "list_utils.map_cons". auto. Qed.

Definition concat {T}: list (list T) -> list T := fold_right (@app _) nil.

Lemma concat_app T (x y: list (list T)): concat (x ++ y) = concat x ++ concat y.
Proof with auto. hammer_hook "list_utils" "list_utils.concat_app".
induction x...
simpl.
intros.
rewrite IHx.
rewrite app_ass...
Qed.

Lemma In_concat X (l: list (list X)) (s: list X) (x: X): In x s -> In s l -> In x (concat l).
Proof with auto. hammer_hook "list_utils" "list_utils.In_concat".
induction l...
intros.
simpl.
apply in_or_app.
inversion_clear H0.
subst...
right...
Qed.

Lemma In_concat_inv X (x: X) (l: list (list X)):
In x (concat l) -> exists s, In x s /\ In s l.
Proof with auto. hammer_hook "list_utils" "list_utils.In_concat_inv".
induction l.
intros.
elimtype False...
simpl.
intros.
destruct (in_app_or _ _ _ H).
exists a.
split...
destruct (IHl H0).
destruct H1.
exists x0...
Qed.

Definition eq_count X (d: forall (x y: X), { x = y } + { x <> y }) (x: X): list X -> nat :=
count (fun y => unsum_bool (d x y)).

Lemma eq_count_0 X (d: forall (x y: X), { x = y } + { x <> y }) (x: X) l:
~ In x l -> eq_count d x l = 0%nat.
Proof with auto. hammer_hook "list_utils" "list_utils.eq_count_0".
induction l...
simpl.
intros.
destruct (d x a).
elimtype False.
apply H.
left...
simpl.
apply IHl.
intro.
apply H.
right...
Qed.

Lemma eq_count_NoDup X (d: forall (x y: X), { x = y } + { x <> y }) (x: X) l:
NoDup l -> eq_count d x l <= 1.
Proof with auto. hammer_hook "list_utils" "list_utils.eq_count_NoDup".
induction l...
simpl.
intros.
inversion_clear H...
destruct (d x a); simpl...
subst.
rewrite eq_count_0...
Qed.

Lemma NoDup_incl_Permutation A (a b: list A):
length a = length b -> NoDup a -> incl a b -> Permutation a b.
Proof with auto. hammer_hook "list_utils" "list_utils.NoDup_incl_Permutation".
induction a in b |- *; intros.
destruct b.
apply perm_nil.
discriminate.
assert (In a b).
apply H1.
left...
destruct (In_inv_perm a b H2).
apply perm_trans with (a :: x)...
apply perm_skip.
apply IHa.
cset (Permutation_length H3).
rewrite <- H in H4.
inversion_clear H4...
inversion_clear H0...
cut (incl a0 (a :: x)).
intros.
intro.
intros.
cset (H4 a1 H5).
inversion_clear H6...
subst.
inversion_clear H0.
elimtype False...
apply incl_tran with b...
intro.
intros.
apply H1.
right...
apply Permutation_incl.
apply Permutation_sym...
Qed.

Lemma NoDup_map' A B (f: A -> B) (l: list A):
(forall x y: A, In x l -> In y l -> x <> y -> f x <> f y) ->
NoDup l -> NoDup (map f l).
Proof with auto. hammer_hook "list_utils" "list_utils.NoDup_map'".
induction l; simpl...
intros.
inversion_clear H0.
apply NoDup_cons...
intro.
destruct (In_map_inv H0).
destruct H3.
apply (H x a)...
intro.
subst...
Qed.

Lemma NoDup_map A B (f: A -> B) l:
(forall x y, In x l -> In y l -> f x = f y -> x = y) -> NoDup l -> NoDup (map f l).
Proof with simpl; auto. hammer_hook "list_utils" "list_utils.NoDup_map".
induction l...
intros.
simpl.
inversion_clear H0.
apply NoDup_cons...
intro.
apply H1.
destruct (In_map_inv H0).
destruct H3.
rewrite (H a x)...
Qed.

Inductive InP (X: Type) (P: X -> Prop): list X -> Prop :=
| InP_head x t: P x -> InP P (x :: t)
| InP_tail x t: InP P t -> InP P (x :: t).

Inductive NoDupL (A: Type): list (list A) -> Prop :=
| NoDupL_nil: NoDupL nil
| NoDupL_cons (l: list A) (ll: list (list A)): NoDup l ->
(forall x, In x l -> ~ InP (In x) ll) -> NoDupL ll -> NoDupL (l :: ll).

Hint Constructors NoDupL.

Lemma InP_In (X: Type) (l: list X) (ll: list (list X)): In l ll -> forall x, In x l -> InP (In x) ll.
Proof with auto. hammer_hook "list_utils" "list_utils.InP_In".
induction ll.
intros.
inversion H.
intros.
inversion_clear H; [left | right]...
subst...
Qed.

Lemma InP_In_inv X (x: X) (ll: list (list X)):
InP (In x) ll -> exists l, In x l /\ In l ll.
Proof with auto. hammer_hook "list_utils" "list_utils.InP_In_inv".
intros H.
induction H.
exists x0.
split...
left...
destruct IHInP.
destruct H0.
exists x1.
split...
right...
Qed.

Arguments InP_In_inv [X x ll].

Lemma NoDup_concat A (l: list (list A)): NoDupL l -> NoDup (concat l).
Proof with auto. hammer_hook "list_utils" "list_utils.NoDup_concat".
induction l; simpl; intros.
apply NoDup_nil.
inversion_clear H.
induction a...
inversion_clear H0.
simpl.
apply NoDup_cons...
intro.
destruct (in_app_or _ _ _ H0)...
apply (H1 a).
left...
destruct (In_concat_inv _ _ H4).
destruct H5.
apply InP_In with x...
apply IHa...
intros.
apply H1.
right...
Qed.

Lemma In_filter_inv A (f: A -> bool) (x: A) (l: list A): In x (filter f l) -> In x l /\ f x = true.
Proof. hammer_hook "list_utils" "list_utils.In_filter_inv". intros. destruct (filter_In f x l). apply H0. assumption. Qed.

Section Partitioning.

Variable T: Set.

Definition Partitioning: Set := comparison -> list T.

Lemma partition_oblig c l h
(H: {p: Partitioning | Permutation (p Eq ++ p Lt ++ p Gt) l}):
Permutation
((if cmp_cmp c Eq then h :: proj1_sig H Eq else proj1_sig H Eq) ++
(if cmp_cmp c Lt then h :: proj1_sig H Lt else proj1_sig H Lt) ++
(if cmp_cmp c Gt then h :: proj1_sig H Gt else proj1_sig H Gt))
(h :: l).
Proof with auto. hammer_hook "list_utils" "list_utils.partition_oblig".
intros.
destruct H. simpl.
apply Permutation_sym.
cset (Permutation_sym p).
destruct c; simpl.
apply perm_skip...
apply Permutation_cons_app...
rewrite <- app_ass in *.
apply Permutation_cons_app...
Qed.

Definition addToPartitioning (c: comparison) (l: list T) (h: T) (H: {p: Partitioning | Permutation (p Eq ++ p Lt ++ p Gt) l}): {p: Partitioning | Permutation (p Eq ++ p Lt ++ p Gt) (h :: l)} :=
exist (fun p => Permutation (p Eq ++ p Lt ++ p Gt) (h :: l))
(fun c' => if cmp_cmp c c' then h :: proj1_sig H c' else proj1_sig H c')
(partition_oblig c h H).

Definition emp: {p: Partitioning | Permutation (p Eq ++ p Lt ++ p Gt) nil} :=
exist (fun p => Permutation (p Eq ++ p Lt ++ p Gt) nil) (fun _ => nil) (perm_nil T).

End Partitioning.

Fixpoint repeat T (n: nat) (x: T): list T :=
match n with
| 0 => nil
| S n' => x :: repeat n' x
end.

Lemma map_concat T U (l: list (list T)) (f: T -> U): map f (concat l) = concat (map (map f) l).
Proof with auto. hammer_hook "list_utils" "list_utils.map_concat".
induction l...
intros.
simpl.
rewrite map_app.
congruence.
Qed.

Lemma length_0_nil A (l: list A): length l = 0%nat <-> l = nil.
Proof with auto. hammer_hook "list_utils" "list_utils.length_0_nil".
intuition.
destruct l...
discriminate.
subst...
Qed.

Lemma length_ne_0_ne_nil A (l: list A): length l <> 0%nat -> l <> nil.
Proof. hammer_hook "list_utils" "list_utils.length_ne_0_ne_nil". destruct l. auto. intros. discriminate. Qed.

Inductive elemsR A B (R: A -> B -> Prop): list A -> list B -> Prop :=
| eR_nil: elemsR R nil nil
| eR_cons (a: A) (b: B): R a b -> forall l l', elemsR R l l' -> elemsR R (a :: l) (b :: l').

Hint Constructors elemsR.

Instance elemsR_trans A `{R: relation A} {TR: Transitive R}: Transitive (elemsR R).
Proof with auto. hammer_hook "list_utils" "list_utils.elemsR_trans".
intro.
induction x.
intros.
destruct y...
inversion H.
intros.
destruct y.
inversion H.
destruct z.
inversion H0.
inversion_clear H.
inversion_clear H0.
apply eR_cons...
transitivity a0...
apply IHx with y...
Qed.

Lemma elemsR_le_S a b: elemsR le a b -> elemsR le (map S a) (map S b).
Proof. hammer_hook "list_utils" "list_utils.elemsR_le_S". intros. induction H; simpl; auto with arith. Qed.

Lemma elemsR_map A (R: relation A) f l:
(forall x, In x l -> R (f x) x) -> elemsR R (map f l) l.
Proof. hammer_hook "list_utils" "list_utils.elemsR_map". induction l; simpl; intuition. Qed.

Lemma elemsR_map_map (X Y: Type) (f g: Y -> X) (l: list Y) (R: relation X): (forall x, In x l -> R (f x) (g x)) -> elemsR R (map f l) (map g l).
Proof with auto. hammer_hook "list_utils" "list_utils.elemsR_map_map".
induction l. simpl...
intros.
apply eR_cons; intuition.
Qed.

Lemma elemsR_impl A (R R' : relation A): (forall x y: A, R x y -> R' x y) -> forall l l', elemsR R l l' -> elemsR R' l l'.
Proof. hammer_hook "list_utils" "list_utils.elemsR_impl". induction l; intros; inversion_clear H0; auto. Qed.

Section Permuted.

Context {A: Type} (R: relation A).

Inductive Permuted: relation (list A) :=
| permuted_nil : Permuted nil nil
| permuted_skip : forall (x x': A), R x x' -> forall (l l' : list A), Permuted l l' -> Permuted (x :: l) (x' :: l')
| permuted_swap : forall (x y: A) (l: list A), Permuted (y :: x :: l) (x :: y :: l)
| permuted_trans : forall l l' l'' : list A, Permuted l l' -> Permuted l' l'' -> Permuted l l''.

Hint Constructors Permuted.

Context {Rrefl: Reflexive R}.

Lemma permuted_refl l: Permuted l l.
Proof. hammer_hook "list_utils" "list_utils.permuted_refl". induction l; auto. Qed.

Hint Immediate permuted_refl.

Lemma elemsR_permuted l l': elemsR R l l' -> Permuted l l'.
Proof. hammer_hook "list_utils" "list_utils.elemsR_permuted". induction l in l' |- *; intros; inversion_clear H; auto. Qed.

Lemma alt_permuted_swap (x x' y y': A): R x x' -> R y y' ->
forall (l l': list A), elemsR R l l' -> Permuted (y :: x :: l) (x' :: y' :: l').
Proof with auto. hammer_hook "list_utils" "list_utils.alt_permuted_swap".
intros.
apply permuted_trans with (y' :: x' :: l)...
apply permuted_trans with (y' :: x' :: l')...
apply permuted_skip...
apply permuted_skip...
apply elemsR_permuted...
Qed.

End Permuted.

Hint Constructors Permuted.

Lemma map_map_comp A B C (f: A -> B) (g: B -> C) (l: list A):
map g (map f l) = map (g ∘ f) l.
Proof. hammer_hook "list_utils" "list_utils.map_map_comp".
intros.
rewrite map_map.
reflexivity.
Qed.

Lemma concat_map_singleton A (l: list A): concat (map (fun x => x :: nil) l) = l.
Proof. hammer_hook "list_utils" "list_utils.concat_map_singleton".
induction l. intuition.
simpl. congruence.
Qed.

Lemma Permuted_sub A (R: relation A) x y: Permuted R x y -> forall (R': relation A), (forall x y, R x y -> R' x y) -> Permuted R' x y.
Proof with auto. hammer_hook "list_utils" "list_utils.Permuted_sub".
intros.
induction H...
apply permuted_trans with l'...
Qed.

Lemma Permuted_map A B (R: relation B) (f: A -> B): Proper (Permuted (on f R) ==> Permuted R) (map f).
Proof. hammer_hook "list_utils" "list_utils.Permuted_map". repeat intro. induction H; simpl; eauto. Qed.

Definition add := fold_right plus (0%nat).

Lemma add_same c l: (forall x, In x l -> x = c) -> add l = length l * c.
Proof with auto. hammer_hook "list_utils" "list_utils.add_same".
induction l...
intros.
simpl.
intuition.
Qed.

Lemma length_concat T (l: list (list T)):
length (concat l) = add (map (@length _) l).
Proof with auto. hammer_hook "list_utils" "list_utils.length_concat".
induction l...
simpl.
rewrite app_length, IHl...
Qed.

Lemma concat_map_nil T U (l: list T): concat (map (fun _ => nil) l) = @nil U.
Proof. hammer_hook "list_utils" "list_utils.concat_map_nil". induction l; auto. Qed.

Definition product A B (aa: list A) (bb: list B): list (A * B) :=
concat (map (fun a => map (pair a) bb) aa).

Instance Permutation_concat T: Proper (Permutation ==> Permutation) (@concat T).
Proof with auto. hammer_hook "list_utils" "list_utils.Permutation_concat".
repeat intro.
induction H...
simpl.
apply Permutation_app...
simpl.
repeat rewrite <- app_ass.
apply Permutation_app...
apply Permutation_app_swap.
eauto.
Qed.

Lemma concat_map_singleton_f T A (f: A -> T) l: concat (map (fun x : A => (f x)::nil) l) = map f l.
Proof with auto. hammer_hook "list_utils" "list_utils.concat_map_singleton_f".
induction l...
simpl.
congruence.
Qed.

Lemma map_concat_map T U V (g: T -> list U) (f: U -> V) l:
map f (concat (map g l)) = concat (map (map f ∘ g) l).
Proof with auto. hammer_hook "list_utils" "list_utils.map_concat_map".
unfold Basics.compose.
induction l...
simpl.
rewrite map_app.
congruence.
Qed.

Lemma concat_concat T (x: list (list (list T))):
concat (concat x) = concat (map concat x).
Proof with auto. hammer_hook "list_utils" "list_utils.concat_concat".
induction x...
simpl.
rewrite concat_app.
congruence.
Qed.

Section two_lists_rect.

Variables (T: Type) (P: list T -> list T -> Type)
(Pnil_l: forall x, P nil x) (Pnil_r: forall x, P x nil)
(Pcons: forall x x' y y', P x' (y :: y') -> P (x :: x') y' -> P (x :: x') (y :: y')).

Let R: relation (list T * list T) := pair_rel (ltof (list T) (@length _)) (ltof (list T) (@length _)).

Let wf_R: well_founded R.
Proof. hammer_hook "list_utils" "list_utils.two_lists_rect.wf_R". apply well_founded_pairs; apply well_founded_ltof. Qed.

Lemma two_lists_rect_pre (p: list T * list T): P (fst p) (snd p).
Proof with auto. hammer_hook "list_utils" "list_utils.two_lists_rect_pre".
apply (well_founded_induction_type wf_R (fun p => P (fst p) (snd p))).
unfold R, ltof.
destruct x as [[|A] [|B]]...
intros.
simpl.
apply Pcons.
apply (X (l, B :: l0)).
apply pair_rel_l...
apply (X (A :: l, l0)).
apply pair_rel_r...
Defined.

Definition two_lists_rect x y: P x y := two_lists_rect_pre (x, y).

End two_lists_rect.

Instance Reflexive_Permutation T: Reflexive Permutation := @Permutation_refl T.
Instance Reflexive_Symmetric T: Symmetric Permutation := @Permutation_sym T.
Instance Reflexive_Transitive T: Transitive Permutation := @perm_trans T.

Instance app_Permutation_mor T: Proper (Permutation ==> Permutation ==> Permutation) (@app T).
Proof. hammer_hook "list_utils" "list_utils.app_Permutation_mor". repeat intro. apply Permutation_app; assumption. Qed.

Instance map_Permutation_mor T U (f: T -> U): Proper (Permutation ==> Permutation) (map f) :=
Permutation_map f.

Lemma concatMap_concatMap' T U V (g: T -> list U) (f: U -> list V) l:
concat (map f (concat (map g l))) = concat (map (concat ∘ map f ∘ g) l).
Proof with auto. hammer_hook "list_utils" "list_utils.concatMap_concatMap'".
induction l...
simpl.
rewrite <- IHl.
unfold Basics.compose.
rewrite map_app.
rewrite concat_app...
Qed.

Lemma Permutation_concatMap T U (f g: T -> list U) l:
(forall x, In x l -> Permutation (f x) (g x)) ->
Permutation (concat (map f l)) (concat (map g l)).
Proof with auto. hammer_hook "list_utils" "list_utils.Permutation_concatMap".
induction l...
simpl.
intros.
rewrite IHl...
rewrite H...
Qed.

Hint Resolve Permutation_concat.

Lemma Permutation_concat_map_app T A (f g: A -> list T) l:
Permutation (concat (map (fun x => f x ++ g x) l)) (concat (map f l ++ map g l)).
Proof with auto. hammer_hook "list_utils" "list_utils.Permutation_concat_map_app".
induction l...
simpl.
rewrite IHl.
repeat rewrite concat_app.
simpl.
rewrite app_ass.
apply Permutation_app...
rewrite Permutation_app_swap.
rewrite app_ass.
apply Permutation_app...
apply Permutation_app_swap.
Qed.

Lemma concat_product T U V (f: U -> T -> list V) l l':
Permutation
(concat (map (fun x => concat (map (fun y => f y x) l')) l))
(concat (map (fun x => concat (map (f x) l)) l')).
Proof with auto. hammer_hook "list_utils" "list_utils.concat_product".
induction l...
intros.
simpl.
rewrite concat_map_nil...
intros.
simpl.
rewrite IHl.
apply Permutation_sym.
rewrite Permutation_concat_map_app.
rewrite concat_app...
Qed.

Instance map_eq_morphism A B: Proper (pointwise_relation _ eq ==> eq ==> eq) (@map A B).
Proof with auto. hammer_hook "list_utils" "list_utils.map_eq_morphism".
repeat intro.
subst.
induction y0...
simpl.
congruence.
Qed.

Section splits_and_perms.

Context {T: Type}.

Fixpoint splits (l: list T): list (T * list T) :=
match l with
| nil => nil
| h :: t => (h, t) :: map (fun xy => (fst xy, h :: snd xy)) (splits t)
end.

Lemma length_splits l: length (splits l) = length l.
Proof with auto. hammer_hook "list_utils" "list_utils.length_splits".
induction l...
simpl.
rewrite map_length.
intuition.
Qed.

Lemma splits_are_perms l p: In p (splits l) -> Permutation (fst p :: snd p) l.
Proof with auto. hammer_hook "list_utils" "list_utils.splits_are_perms".
induction l in p |- *...
simpl.
intuition.
simpl.
intros.
destruct H.
subst...
destruct (fst (conj_prod (in_map_iff _ _ _)) H).
destruct H0.
apply IHl in H1.
subst.
simpl...
apply perm_trans with (a :: fst x :: snd x).
apply perm_swap.
apply perm_skip...
Qed.

Lemma length_in_splits l p: In p (splits l) -> S (length (snd p)) = length l.
Proof. hammer_hook "list_utils" "list_utils.length_in_splits".
intros.
apply splits_are_perms in H.
exact (Permutation_length H).
Qed.

Fixpoint insert_everywhere (x: T) (l: list T): list (list T) :=
match l with
| nil => (x :: nil) :: nil
| h :: t => (x :: h :: t) :: map (cons h) (insert_everywhere x t)
end.

Lemma insert_everywhere_are_perms x l:
forall y, In y (insert_everywhere x l) -> Permutation y (x :: l).
Proof with auto. hammer_hook "list_utils" "list_utils.insert_everywhere_are_perms".
induction l...
intros.
simpl in H.
intuition.
subst...
intros.
simpl in H.
destruct H.
subst...
apply in_map_iff in H. destruct H as [x0 [A B]].
subst.
apply IHl in B.
eauto.
Qed.

Lemma length_insert_everywhere x l:
length (insert_everywhere x l) = S (length l).
Proof with auto. hammer_hook "list_utils" "list_utils.length_insert_everywhere".
induction l...
simpl.
rewrite map_length.
congruence.
Qed.

Definition perms: list T -> list (list T)
:= fold_right (fun h => concat ∘ map (insert_everywhere h)) (nil :: nil).

Lemma perms_are_perms l a: In a (perms l) -> Permutation a l.
Proof with auto. hammer_hook "list_utils" "list_utils.perms_are_perms".
induction l in a |- *.
simpl.
intuition.
subst...
intros.
simpl in H.
unfold Basics.compose in H.
apply In_concat_inv in H. destruct H. destruct H.
apply in_map_iff in H0. destruct H0 as [x0 [A B]].
subst.
eauto using insert_everywhere_are_perms.
Qed.

Lemma length_perms l: length (perms l) = fact (length l).
Proof with auto. hammer_hook "list_utils" "list_utils.length_perms".
induction l...
simpl.
unfold Basics.compose.
rewrite length_concat.
rewrite map_map.
rewrite (@add_same (S (length l)) (map (fun x => length (insert_everywhere a x)) (perms l))).
rewrite map_length.
rewrite IHl.
rewrite Mult.mult_comm...
intros.
destruct (in_map_iff (fun x => length (insert_everywhere a x)) (perms l) x).
clear H1.
apply H0 in H. clear H0.
destruct H. destruct H.
subst.
rewrite length_insert_everywhere.
f_equal.
apply Permutation_length.
apply perms_are_perms...
Qed.

Definition alt_perms l: list (list T) :=
match l with
| nil => nil :: nil
| _ => concat (map (fun p => (map (cons (fst p)) (perms (snd p)))) (splits l))
end.

Lemma splits_permuted (l l': list T): Permutation l l' ->
Permuted (fun x y => fst x = fst y /\ Permutation (snd x) (snd y)) (splits l) (splits l').
Proof with auto. hammer_hook "list_utils" "list_utils.splits_permuted".
intro.
set (fun x y: T * list T => fst x = fst y /\ Permutation (snd x) (snd y)).
intros.
induction H.
simpl...
simpl.
apply permuted_skip...
split...
apply Permuted_map.
unfold on.
subst P.
simpl.
apply (Permuted_sub IHPermutation).
intuition.
simpl.
subst P.
apply alt_permuted_swap...
repeat rewrite map_map.
simpl.
apply elemsR_map_map.
simpl...
eauto.
Qed.

Inductive merges_spec: list T -> list T -> list (list T) -> Prop :=
| merges_left_nil x: merges_spec nil x (x :: nil)
| merges_right_nil x: merges_spec x nil (x :: nil)
| merges_cons x y h t r r':
merges_spec y (h :: t) r ->
merges_spec (x :: y) t r' ->
merges_spec (x :: y) (h :: t) (map (cons x) r ++ map (cons h) r').

Hint Constructors merges_spec.

Lemma merges_uniq a b r:
merges_spec a b r ->
forall r', merges_spec a b r' -> r = r'.
Proof with auto. hammer_hook "list_utils" "list_utils.merges_uniq".
intros H.
induction H; intros.
inversion_clear H...
inversion_clear H...
inversion_clear H1.
apply IHmerges_spec1 in H2.
apply IHmerges_spec2 in H3.
congruence.
Qed.

Lemma length_merges (F: nat -> nat -> nat) a b r:
(forall n, F 0 n = 1) ->
(forall n, F n 0 = 1) ->
(forall n n', F n (S n') + F (S n) n' = F (S n) (S n')) ->
merges_spec a b r -> length r = F (length a) (length b).
Proof with auto. hammer_hook "list_utils" "list_utils.length_merges".
intros.
induction H2.
simpl...
simpl...
rewrite app_length.
repeat rewrite map_length.
rewrite IHmerges_spec1. clear IHmerges_spec1.
rewrite IHmerges_spec2. clear IHmerges_spec2.
simpl @length...
Qed.

Definition me (ab: list T * list T): nat := length (fst ab) + length (snd ab).

Program Fixpoint merges_ex (ab: list T * list T) {measure (me ab)}: sig (merges_spec (fst ab) (snd ab)) :=
match ab with
| (nil, x) => x :: nil
| (x, nil) => x :: nil
| (x :: y, h :: t) => map (cons x) (merges_ex (y, h :: t)) ++ map (cons h) (merges_ex (x :: y, t))
end.

Next Obligation. unfold me. simpl. omega. Qed.
Next Obligation. repeat destruct_call merges_ex; auto. Qed.

Definition merges (a b: list T): list (list T) := proj1_sig (merges_ex (a, b)).

Lemma merges_real_eq a b: merges a b =
match a, b with
| nil, x => x :: nil
| x, nil => x :: nil
| x :: y, h :: t => map (cons x) (merges y (h :: t)) ++ map (cons h) (merges (x :: y) t)
end.
Proof with auto. hammer_hook "list_utils" "list_utils.merges_real_eq".
intros.
apply (@merges_uniq a b).
unfold merges. destruct_call merges_ex...
destruct a... destruct b...
unfold merges. repeat destruct_call merges_ex...
Qed.

Lemma merges_nil_r a: merges a [] = [a].
Proof with auto. hammer_hook "list_utils" "list_utils.merges_nil_r".
intros.
rewrite merges_real_eq.
destruct a...
Qed.

Hint Resolve Permutation_concat.

Lemma product_app: forall T (a b c: list T), product (a ++ b) c = product a c ++ product b c.
Proof with auto. hammer_hook "list_utils" "list_utils.product_app".
intros.
unfold product.
rewrite map_app.
rewrite concat_app...
Qed.

Lemma product_concat: forall T (a: list (list T)) (b: list T), product (concat a) b = concat (map (flip (@product _ _) b) a).
Proof with auto. hammer_hook "list_utils" "list_utils.product_concat".
induction a...
simpl.
unfold flip at 1.
intros.
rewrite <- IHa.
apply product_app.
Qed.

Lemma concatMap_insert_everywhere_comm x y l: Permutation
(concat (map (insert_everywhere x) (insert_everywhere y l)))
(concat (map (insert_everywhere y) (insert_everywhere x l))).
Proof with auto. hammer_hook "list_utils" "list_utils.concatMap_insert_everywhere_comm".
induction l...
simpl...
simpl.
rewrite perm_swap.
apply perm_skip.
apply perm_skip.
rewrite (map_map (cons a) (insert_everywhere x)).
rewrite (map_map (cons a) (insert_everywhere y)).
simpl.
rewrite (Permutation_concat_map_app (fun x0 => (x :: a :: x0) :: nil) (fun x0 => map (cons a) (insert_everywhere x x0)) (insert_everywhere y l)).
apply Permutation_sym.
rewrite (Permutation_concat_map_app (fun x0 => (y :: a :: x0) :: nil) (fun x => map (cons a) (insert_everywhere y x)) (insert_everywhere x l)).
repeat rewrite concat_app.
repeat rewrite concat_map_singleton_f.
rewrite <- (map_map (insert_everywhere x) (map (cons a))).
rewrite <- (map_map (insert_everywhere y) (map (cons a))).
repeat rewrite <- map_concat.
repeat rewrite map_map.
repeat rewrite <- app_ass.
symmetry in IHl...
apply Permutation_app...
apply Permutation_app_swap.
Qed.

Instance Permutation_perms: Proper (Permutation ==> Permutation) perms.
Proof with eauto 2. hammer_hook "list_utils" "list_utils.Permutation_perms".
intros l l' P.
induction P...
simpl.
apply Permutation_concat...
simpl.
unfold Basics.compose.
set (perms l). clearbody l0. clear l. rename l0 into l.
repeat rewrite concatMap_concatMap'.
apply Permutation_concatMap.
intros.
unfold Basics.compose.
apply concatMap_insert_everywhere_comm.
Qed.

Lemma merges_insert_everywhere a l: insert_everywhere a l = merges (a :: nil) l.
Proof with auto. hammer_hook "list_utils" "list_utils.merges_insert_everywhere".
induction l...
simpl.
rewrite IHl.
rewrite (merges_real_eq [a] (a0::l)).
rewrite (merges_real_eq [] (a0::l)).
simpl...
Qed.

Lemma merges_insert_everywhere' a l: Permutation (insert_everywhere a l) (merges l (a :: nil)).
Proof with auto. hammer_hook "list_utils" "list_utils.merges_insert_everywhere'".
induction l...
simpl.
transitivity ((a :: a0 :: l) :: map (cons a0) (merges l [a]))...
rewrite (merges_real_eq (a0::l) [a]).
rewrite (merges_real_eq (a0::l) []).
simpl.
transitivity ([a :: a0 :: l] ++ map (cons a0) (merges l [a]))...
apply Permutation_app_swap.
Qed.

Lemma insert_everywhere_merges_commute a x y: Permutation
(concat (map (insert_everywhere a) (merges y x)))
(concat (map (merges y) (insert_everywhere a x))).

Proof with auto. hammer_hook "list_utils" "list_utils.insert_everywhere_merges_commute".
revert x y.
apply two_lists_rect; intros.
simpl.
rewrite merges_nil_r.
simpl.
repeat rewrite app_nil_r.
apply merges_insert_everywhere'.
simpl.
rewrite app_nil_r.
rewrite (map_ext (merges []) (fun x0 => [x0])).
rewrite concat_map_singleton...
intros.
apply merges_real_eq.
rewrite (merges_real_eq (y :: y') (x :: x')).
rewrite map_app.
rewrite concat_app.
repeat rewrite map_map.
simpl insert_everywhere.
rewrite (Permutation_concat_map_app (fun x0 => [a :: y :: x0]) (fun x0 => map (cons y) (insert_everywhere a x0))).
rewrite (Permutation_concat_map_app (fun x0 => [a :: x :: x0]) (fun x0 => map (cons x) (insert_everywhere a x0))).
repeat rewrite concat_app.
repeat rewrite concat_map_singleton_f.
rewrite app_ass.
rewrite <- (map_map (insert_everywhere a) (map (cons x))).
rewrite <- (map_map (insert_everywhere a) (map (cons y))).
rewrite <- map_concat.
rewrite <- map_concat.
rewrite H. rewrite H0.
clear H H0.
simpl @map at 7.
simpl @concat at 3.
rewrite map_map.
rewrite (merges_real_eq (y :: y') (a :: x :: x')).
rewrite (merges_real_eq (y :: y') (x :: x')).
rewrite map_app.
repeat rewrite map_map.
rewrite app_ass.
apply Permutation_sym.
rewrite (Permutation_app_swap (map (cons y) (merges y' (a :: x :: x')))).
repeat rewrite app_ass.
apply Permutation_app...
apply Permutation_sym.
rewrite (Permutation_app_swap (map (cons y) (concat (map (merges y') (insert_everywhere a (x :: x')))))).
repeat rewrite app_ass.
apply Permutation_app...
simpl.
rewrite map_map.
rewrite map_app.
rewrite (map_ext (fun x0 : list T => merges (y :: y') (x :: x0)) (fun x0 : list T => map (cons y) (merges y' (x :: x0)) ++ map (cons x) (merges (y :: y') x0))).
Focus 2.
intros.
rewrite merges_real_eq...
apply Permutation_sym.
rewrite Permutation_concat_map_app.
rewrite concat_app.
rewrite app_ass.
rewrite <- (map_map (fun x0 => merges y' (x :: x0)) (map (cons y))).
rewrite <- map_concat.
rewrite Permutation_app_swap.
rewrite <- app_ass.
apply Permutation_app...
rewrite <- (map_map (fun x0 => merges (y :: y') x0) (map (cons x))).
rewrite <- map_concat.
apply Permutation_app...
Qed.

Lemma merges_sym x y: Permutation (merges x y) (merges y x).
Proof with auto. hammer_hook "list_utils" "list_utils.merges_sym".
intros.
unfold merges at 1.
destruct_call merges_ex.
simpl in *.
induction m...
rewrite merges_nil_r...
rewrite IHm1.
rewrite IHm2.
rewrite (merges_real_eq (h :: t) (x :: y)).
apply Permutation_app_swap.
Qed.

Hint Immediate merges_sym.

Lemma perms_app (a b: list T): Permutation (perms (a ++ b)) (concat (map (uncurry merges) (product (perms a) (perms b)))).
Proof with auto. hammer_hook "list_utils" "list_utils.perms_app".
unfold product.
intros.
rewrite map_concat.
rewrite map_map.
induction a.
simpl.
rewrite app_nil_r.
rewrite map_map.
unfold uncurry.
simpl.
rewrite (map_ext (fun x => merges [] x) (fun x => x :: nil))...
rewrite concat_map_singleton...
simpl.
unfold Basics.compose.
rewrite IHa. clear IHa.
rewrite (map_ext (fun x : list T => map (uncurry merges) (map (pair x) (perms b)))
(fun x : list T => map (merges x) (perms b))).
rewrite (map_ext (fun x : list T => map (uncurry merges) (map (pair x) (perms b)))
(fun x : list T => map (merges x) (perms b))).
rewrite concat_concat.
rewrite concat_concat.
rewrite map_map.
rewrite map_map.
rewrite map_concat_map.
rewrite concat_concat.
rewrite map_map.
rewrite map_concat_map.
rewrite concat_concat.
rewrite map_map.
apply Permutation_concatMap.
intros.
unfold Basics.compose.
rewrite map_concat_map.
rewrite concat_concat.
rewrite map_map.
rewrite (map_ext (fun x0 => concat ((map (insert_everywhere a) ∘ merges x) x0))
(concat ∘ (map (insert_everywhere a) ∘ merges x)))...
transitivity (concat (map (concat ∘ map (merges x) ∘ insert_everywhere a) (perms b))).
apply Permutation_concatMap.
intros.
unfold Basics.compose.
apply insert_everywhere_merges_commute.
apply Permutation_sym.
rewrite <- (concat_product merges (perms b) (insert_everywhere a x)).
apply Permutation_concatMap.
intros.
unfold Basics.compose.
apply Permutation_sym.
rewrite <- insert_everywhere_merges_commute.
transitivity (concat (map (merges x0) (insert_everywhere a x))).
apply Permutation_sym.
rewrite <- insert_everywhere_merges_commute...
rewrite merges_sym...
apply Permutation_concatMap.
intros...
intros.
rewrite map_map...
intros.
rewrite map_map...
Qed.

Lemma filter_merges p (x y: list T):
(forall z, In z x -> p z = true) ->
(forall z, In z y -> p z = false) ->
forall r, In r (map (filter p) (merges x y)) -> r = x.
Proof with auto. hammer_hook "list_utils" "list_utils.filter_merges".
pattern x, y.
apply two_lists_rect.
intros.
rewrite merges_real_eq in H1.
simpl in H1.
intuition.
subst.
apply (filter_none p x0)...
intros.
rewrite merges_nil_r in H1.
simpl in H1.
intuition.
subst.
apply filter_all...
intros.
rewrite merges_real_eq in H3.
rewrite map_app in H3.
repeat rewrite map_map in H3.
apply in_app_or in H3.
simpl in H3.
destruct H3.
rewrite H1 in H3.
Focus 2. left...
rewrite <- (map_map (filter p) (cons x0)) in H3.
apply in_map_iff in H3.
destruct H3.
destruct H3.
subst.
f_equal.
apply H...
intuition.
rewrite H2 in H3.
Focus 2. left...
apply H0...
intuition.
Qed.

Instance length_merges_mor: Proper (on length eq ==> on length eq ==> on length eq) merges.
Proof with auto. hammer_hook "list_utils" "list_utils.length_merges_mor".
unfold on.
do 4 intro.
generalize y H. clear y H.
unfold merges at 1.
destruct merges_ex.
simpl in *.
induction m; intros.
destruct y...
discriminate.
destruct y0.
rewrite merges_nil_r...
discriminate.
destruct y0. discriminate.
destruct y1. discriminate.
inversion H.
inversion H0.
rewrite merges_real_eq.
repeat rewrite app_length.
repeat rewrite map_length...
Qed.

Lemma merges_ne_nil x y: merges x y <> nil.
Proof with try discriminate; auto. hammer_hook "list_utils" "list_utils.merges_ne_nil".
intros.
unfold merges.
destruct merges_ex.
simpl in *.
induction m...
destruct r...
Qed.

End splits_and_perms.

Existing Instance Permutation_perms.

Lemma map_repeat A B (f: A -> B) c (l: list A):
(forall x, In x l -> f x = c) -> map f l = repeat (length l) c.
Proof with auto. hammer_hook "list_utils" "list_utils.map_repeat".
induction l...
simpl.
intros.
rewrite IHl...
rewrite H...
Qed.

Lemma repeat_plus T (c: T) n m: repeat (n + m) c = repeat n c ++ repeat m c.
Proof. hammer_hook "list_utils" "list_utils.repeat_plus". induction n. auto. simpl. congruence. Qed.

Lemma concat_repeat T n m (c: T): concat (repeat n (repeat m c)) = repeat (n * m) c.
Proof with auto. hammer_hook "list_utils" "list_utils.concat_repeat".
induction n. auto.
simpl. intros. rewrite IHn, repeat_plus...
Qed.

Lemma filter_perms T p (l: list T):
Permutation
(map (filter p) (perms l))
(concat (map (repeat (fact (length (filter (negb ∘ p) l)) * length (merges (filter p l) (filter (negb ∘ p) l)))) (perms (filter p l)))).

Proof with auto. hammer_hook "list_utils" "list_utils.filter_perms".
intros.
rewrite (complementary_filter_perm p l) at 1.
rewrite perms_app.
rewrite map_concat_map.
unfold product.
rewrite concatMap_concatMap'.
apply Permutation_concatMap.
intros.
unfold Basics.compose.
rewrite map_map.
unfold uncurry.
simpl.
set (t := repeat (length (merges x (filter (fun q => negb (p q)) l))) x).
rewrite (@map_repeat _ _ (fun x0 : list T => map (filter p) (merges x x0)) t (perms (filter (fun x0 : T => negb (p x0)) l))).
rewrite length_perms.
subst t.
rewrite concat_repeat.
pose proof (Permutation_length (perms_are_perms _ _ H)).
rewrite (length_merges_mor H0 refl_equal)...
intros.
rewrite (@map_repeat _ _ (filter p) x (merges x x0)).
subst t.
pose proof (Permutation_length (perms_are_perms _ _ H0)).
rewrite (length_merges_mor refl_equal H1)...
intros.
apply (filter_merges) with p x0...
intros.
apply (filter_In p z l)...
apply Permutation_in with x...
apply perms_are_perms...
intros.
pose proof (Permutation_in _ (perms_are_perms _ _ H0) H2).
cut (negb (p z) = true).
intros.
destruct (p z)...
apply (filter_In (fun q => negb (p q)) z l)...
Qed.

Instance Permutation_length_morphism T: Proper (Permutation ==> eq) (@length T) :=
@Permutation_length T.

Lemma repeat_map_comm A B (f: A -> B) n: ext_eq (map f ∘ repeat n) (repeat n ∘ f).
Proof with auto. hammer_hook "list_utils" "list_utils.repeat_map_comm".
unfold ext_eq.
unfold Basics.compose.
induction n...
simpl in *.
congruence.
Qed.

Lemma length_repeat T (c: T) n: length (repeat n c) = n.
Proof with auto. hammer_hook "list_utils" "list_utils.length_repeat".
induction n...
simpl.
congruence.
Qed.

Hint Immediate length_repeat.

Instance map_ext_eq_mor A B: Proper (@ext_eq A B ==> ext_eq) map.
repeat intro.
apply map_ext.
assumption.
Qed.

Lemma concat_nil X (l: list (list X)): (forall x, In x l -> x = nil) -> concat l = nil.
Proof with intuition. hammer_hook "list_utils" "list_utils.concat_nil".
induction l...
simpl.
rewrite IHl...
rewrite (H a)...
Qed.

Lemma empty_nil X (x: list X): length x = 0%nat -> x = nil.
destruct x.
reflexivity.
intro.
discriminate.
Qed.

Lemma Permuted_Permutation_map T U (R: relation T) (f: T -> U):
(forall x y, R x y -> f x = f y) -> forall a b,
Permuted R a b ->
Permutation (map f a) (map f b).
Proof with auto. hammer_hook "list_utils" "list_utils.Permuted_Permutation_map".
intros.
induction H0...
simpl.
rewrite (H x x')...
eauto.
Qed.

Lemma elemsR_length A (R: A -> A -> Prop) a b (H: elemsR R a b):
length a = length b.
Proof with auto. hammer_hook "list_utils" "list_utils.elemsR_length".
induction H...
simpl.
intuition.
Qed.

Lemma elemsRimpl A B (R: A -> B -> Prop) (l: list A): (forall x, In x l -> sig (R x)) -> sig (elemsR R l).
Proof with intuition; eauto. hammer_hook "list_utils" "list_utils.elemsRimpl".
induction l...
intros.
destruct IHl...
destruct (X a)...
Qed.

Lemma elemsRuniq A B (R: A -> B -> Prop) (l: list A):
(forall x, In x l -> forall y, R x y -> forall y', R x y' -> y = y') -> forall r, elemsR R l r -> forall r', elemsR R l r' -> r = r'.
Proof with intuition; auto. hammer_hook "list_utils" "list_utils.elemsRuniq".
induction l.
intros.
inversion_clear H0. inversion_clear H1...
intros.
inversion_clear H0.
inversion_clear H1.
rewrite (H a) with b b0...
rewrite IHl with l' l'0...
apply H with x...
Qed.

Definition triple0 A B C (t: A * B * C): A := fst (fst t).
Definition triple1 A B C (t: A * B * C): B := snd (fst t).
Definition triple2 A B C (t: A * B * C): C := snd t.

Fixpoint rsplits T (l: list T): list (list T * T * list T) :=
match l with
| nil => nil
| h :: t => (nil, h, t) :: map (fun p => (h :: triple0 p, triple1 p, triple2 p)) (rsplits t)
end.

Lemma splits_rsplits (T: Set) (l: list T): splits l = map (fun p => (triple1 p, triple0 p ++ triple2 p)) (rsplits l).
Proof with auto. hammer_hook "list_utils" "list_utils.splits_rsplits".
induction l...
simpl.
rewrite map_map.
simpl.
rewrite IHl. clear IHl.
unfold triple1.
simpl.
rewrite map_map.
simpl...
Qed.

Lemma insert_everywhere_rsplits (T: Set) (x: T) (l: list T):
insert_everywhere x l =
map (fun x0 => triple0 x0 ++ x :: triple1 x0 :: triple2 x0) (rsplits l) ++ [l ++ [x]].
Proof with auto. hammer_hook "list_utils" "list_utils.insert_everywhere_rsplits".
induction l...
simpl.
rewrite IHl. clear IHl.
unfold triple0, triple1, triple2.
repeat rewrite map_map.
rewrite map_app.
rewrite map_map...
Qed.

Lemma elemsR_map':
forall (A B: Type) (Ra: relation A) (Rb: relation B) (f : A -> B)
(fR: forall x y, Ra x y -> Rb (f x) (f y)) (l l': list A),
elemsR Ra l l' -> elemsR Rb (map f l) (map f l').
Proof. hammer_hook "list_utils" "list_utils.elemsR_map'". intros. induction H; simpl; auto... Qed.

Instance Permutation_cons_morphism A: Proper (eq ==> Permutation ==> Permutation) (@cons A).
Proof with auto. hammer_hook "list_utils" "list_utils.Permutation_cons_morphism".
repeat intro.
subst...
Qed.

Lemma concatMap_insert_everywhere T (x: T) (l: list (list T)):
Permutation
(concat (map (insert_everywhere x) l))
(map (cons x) l ++ concat (map (tail ∘ insert_everywhere x) l)).
Proof with auto. hammer_hook "list_utils" "list_utils.concatMap_insert_everywhere".
induction l...
simpl @concat.
rewrite IHl.
apply Permutation_sym.
rewrite Permutation_app_swap.
unfold compose.
simpl.
rewrite app_ass.
generalize (concat (map (fun x0 : list T => tail (insert_everywhere x x0)) l)). intro.
rewrite (Permutation_app_swap l0).
rewrite <- app_ass.
rewrite <- app_ass.
apply Permutation_app...
destruct a...
simpl.
rewrite Permutation_app_swap.
simpl.
apply perm_skip.
apply Permutation_app_swap.
Qed.

Lemma map_length_filter_permuted_splits T (l l': list T): Permutation l l' ->
forall p,
Permutation
(map (fun x => length (filter (p (fst x)) (snd x))) (splits l))
(map (fun x => length (filter (p (fst x)) (snd x))) (splits l')).
Proof with auto. hammer_hook "list_utils" "list_utils.map_length_filter_permuted_splits".
intros.
apply (@Permuted_Permutation_map (T * list T) nat (fun x y => fst x = fst y /\ Permutation (snd x) (snd y))  (fun x => length (filter (p (fst x)) (snd x)))).
intros.
destruct H0.
destruct x. destruct y.
simpl in H0. subst.
simpl.
simpl in H1.
rewrite H1...
apply splits_permuted...
Qed.

Lemma perms_alt_perms T (l: list T): Permutation (perms l) (alt_perms l).
Proof with auto. hammer_hook "list_utils" "list_utils.perms_alt_perms".
unfold alt_perms.
induction l...
simpl.
unfold Basics.compose.
rewrite concatMap_insert_everywhere.
apply Permutation_app...
rewrite IHl. clear IHl.
destruct l...
rewrite map_concat.
rewrite map_map.
generalize (splits (t :: l)). intro.
setoid_rewrite map_map.
unfold compose.
rewrite concat_concat.
rewrite map_map.
simpl @fst. simpl @snd.
simpl.
unfold compose.
setoid_rewrite map_concat.
setoid_rewrite map_map...
Qed.

Lemma map_single A B (f: A -> B) x: map f [x] = [f x].
Proof. hammer_hook "list_utils" "list_utils.map_single". reflexivity. Qed.

author: lukaszcz

repo: coqhammer-eval


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

(***************************************************************************)
(*                  MUTUAL EXCLUSION OF TWO PROCESSES                      *)
(*                        (Peterson's algorithm)                           *)
(*                                                                         *)
(*                             Eduardo Gimenez                             *)
(*                                (17/03/97)                               *)
(*                                                                         *)
(***************************************************************************)
(*  Proof of soundness : if both processes are equitably scheduled, then   *)
(*  both will go through the critic section an infinite number of times.   *)
(***************************************************************************)

Require Import Bool.
Require Import Streams.
Require Import Def.

(* The definition of Exists in Streams was changed, this file works *)
(* with the old definition *)
Set Implicit Arguments.
Unset Strict Implicit.
Inductive Exists (A : Set) (P : Stream A -> Prop) : Stream A -> Prop :=
  | Here : forall x : Stream A, P x -> Exists P x
  | Further : forall x : Stream A, ~ P x -> Exists P (tl x) -> Exists P x.

Set Strict Implicit.
Unset Implicit Arguments.

Definition is (b : bool) (x : Oracle) := hd x = b.
Definition in_SC (b : bool) (x : Trace) := pc (hd x) b = SC.
Definition Equity (b : bool) := ForAll (Exists (is b)).

(* Some premliminary lemmas *)

Lemma tl_Equity :
 forall (b : bool) (o : Oracle), Equity b o -> Equity b (tl o).
intros b o H; case H; trivial with bool core.
Qed.
Hint Resolve tl_Equity.

Lemma tl_Exists :
 forall (b : bool) (o : Oracle), Equity b o -> Exists (is b) (tl o).
intros b o H; case H.
intros H0 H1.
case H1.
trivial with bool core.
Qed.
Hint Resolve tl_Exists.

Lemma Equity_project :
 forall (b : bool) (o : Oracle), Equity b o -> Exists (is b) o.
intros b o H.
case H; try trivial with bool core.
Qed.
Hint Resolve Equity_project.

(* The states to be treated *)

Notation st := (proc true initial) (only parsing).
Notation stt := (proc true (proc true initial)) (only parsing).
Notation stf := (proc false (proc true initial)) (only parsing).
Notation sttf := (proc false (proc true (proc true initial))) (only parsing).
Notation sf := (proc false initial) (only parsing).
Notation sft := (proc true (proc false initial)) (only parsing).
Notation sff := (proc false (proc false initial)) (only parsing).
Notation sfft := (proc true (proc false (proc false initial))) (only parsing).
Notation sfff := (proc false (proc false (proc false initial)))
  (only parsing).

Section The_Cycle.

Variable b b1 : bool.
Inductive Cycle : Memo -> Prop :=
  | cf : b1 <> b -> Cycle (proc b1 initial)
  | cff : b1 <> b -> Cycle (proc b1 (proc b1 initial))
  | cfff : b1 <> b -> Cycle (proc b1 (proc b1 (proc b1 initial))).

End The_Cycle.
Hint Resolve cf cff cfff.

(*************************************************************
   The proof consists in finding a path from each of the
   possible states to another state that satisfies the
   condition in_SC. Such paths are constructed bottom-up,
   starting from the states where the condition is satisfied.
   Several inductions are needed to avoid getting into infinite
   loops due to non-equitable scheduling. The following lemmas
   construct up the paths for each node.

 ****************************************************************)

(* Some useful tacticals *)

Ltac SolveHere := constructor 1; unfold in_SC in |- *; auto with bool core.

Ltac SolveFurther eq :=
  constructor 2;
   [ unfold in_SC in |- *; simpl in |- *; discriminate
   | simpl in |- *; rewrite eq; simpl in |- *; auto with bool ].

Ltac SolveSimpleNode :=
  intros o H; constructor 2;
   [ unfold in_SC in |- *; simpl in |- *; discriminate
   | simpl in |- *; case (hd o); auto with bool core ].

Ltac SolveCycleNode H eq2 :=
  elim H;
   [ unfold is in |- *; intros x theeq; SolveFurther theeq;
      auto with bool datatypes
   | intros x diseq nomatters hypind; SolveFurther (eq2 (hd x));
      auto with bool datatypes ].

Ltac SolveCycleNode1 H :=
  elim H;
   [ unfold is in |- *; intros x theeq; SolveFurther theeq;
      auto with bool datatypes
   | intros x diseq nomatters hypind ].

(* Paths for the first process *)

Lemma fnttf1 :
 forall o : Oracle,
 Exists (in_SC true)
   (protocol (proc false (proc true (proc true initial))) o).
intro b.
 SolveHere.
Qed.
Hint Resolve fnttf1.

Lemma fntf1 :
 forall o : Oracle,
 Exists (is true) o ->
 Exists (in_SC true) (protocol (proc false (proc true initial)) o).
intros o H.
SolveCycleNode H not_true_is_false.
Qed.
Hint Resolve fntf1.

Lemma fntt1 :
 forall o : Oracle,
 Exists (in_SC true) (protocol (proc true (proc true initial)) o).
 SolveHere.
Qed.
Hint Resolve fntt1.

Lemma fnt1 :
 forall o : Oracle,
 Equity true o -> Exists (in_SC true) (protocol (proc true initial) o).
 SolveSimpleNode.
Qed.
Hint Resolve fnt1.

Lemma fnfft1 :
 forall o : Oracle,
 (forall b : bool, Equity b o) ->
 Exists (in_SC true)
   (protocol (proc true (proc false (proc false initial))) o).
intros o1 H.
cut (Equity false o1); auto with bool core.
intros H1.
inversion_clear H1.
generalize H; clear H.
SolveCycleNode H0 not_false_is_true.
Qed.
Hint Resolve fnfft1.

Lemma fnft1 :
 forall o : Oracle,
 (forall b : bool, Equity b o) ->
 Exists (in_SC true) (protocol (proc true (proc false initial)) o).
intros o1 H.
cut (Equity false o1); auto with bool core.
intros H1.
inversion_clear H1.
generalize H; clear H.
SolveCycleNode H0 not_false_is_true.
Qed.
Hint Resolve fnft1.

Lemma fnf1 :
 forall o : Oracle,
 (forall b : bool, Equity b o) ->
 forall m : Memo, Cycle true false m -> Exists (in_SC true) (protocol m o).
simpl in |- *; intros o H.
cut (Equity true o); auto with bool core.
intros H1.
inversion_clear H1.
generalize H; clear H.
elim H0.
unfold is in |- *.
intros x eq H m whichm.
case whichm; SolveFurther eq.
intros x diseq H hypind H1 m whichm.
case whichm; SolveFurther (not_true_is_false (hd x)); auto with bool core.
apply hypind; auto.
apply (cf true false); auto with bool core.
Qed.
Hint Resolve fnf1.

Lemma fninit1 :
 forall o : Oracle,
 (forall b : bool, Equity b o) -> Exists (in_SC true) (protocol initial o).
 SolveSimpleNode.
Qed.
Hint Resolve fninit1.

(* Paths for the second process *)

Lemma fnfft2 :
 forall o : Oracle,
 Exists (in_SC false)
   (protocol (proc true (proc false (proc false initial))) o).
 SolveHere.
Qed.
Hint Resolve fnfft2.

Lemma fnff2 :
 forall o : Oracle,
 Exists (in_SC false) (protocol (proc false (proc false initial)) o).
 SolveHere.
Qed.
Hint Resolve fnff2.

Lemma fnft2 :
 forall o : Oracle,
 Exists (is false) o ->
 Exists (in_SC false) (protocol (proc true (proc false initial)) o).
intros o H.
SolveCycleNode H not_false_is_true.
Qed.
Hint Resolve fnft2.

Lemma fnf2 :
 forall o : Oracle,
 Equity false o -> Exists (in_SC false) (protocol (proc false initial) o).
 SolveSimpleNode.
Qed.
Hint Resolve fnf2.

Lemma fnttf2 :
 forall o : Oracle,
 (forall b : bool, Equity b o) ->
 Exists (in_SC false)
   (protocol (proc false (proc true (proc true initial))) o).
intros o1 H.
cut (Equity true o1); auto with bool core.
intros H1.
inversion_clear H1.
generalize H; clear H.
SolveCycleNode H0 not_true_is_false.
Qed.
Hint Resolve fnttf2.

Lemma fntf2 :
 forall o : Oracle,
 (forall b : bool, Equity b o) ->
 Exists (in_SC false) (protocol (proc false (proc true initial)) o).
intros o1 H.
cut (Equity true o1); auto with bool core.
intros H1.
inversion_clear H1.
generalize H; clear H.
SolveCycleNode H0 not_true_is_false.
Qed.
Hint Resolve fntf2.

Lemma fntt2 :
 forall o : Oracle,
 (forall b : bool, Equity b o) ->
 forall m : Memo, Cycle false true m -> Exists (in_SC false) (protocol m o).
simpl in |- *; intros o H.
cut (Equity false o); auto with bool core.
intros H1.
inversion_clear H1.
generalize H; clear H.
elim H0.
unfold is in |- *.
intros x eq H m whichm.
case whichm; SolveFurther eq.
intros x diseq H hypind H1 m whichm.
case whichm; SolveFurther (not_false_is_true (hd x)); auto with bool core.
Qed.
Hint Resolve fntt2.

Lemma fninit2 :
 forall o : Oracle,
 (forall b : bool, Equity b o) -> Exists (in_SC false) (protocol initial o).
 SolveSimpleNode.
Qed.
Hint Resolve fninit2.

Lemma fnfff2 :
 forall o : Oracle,
 (forall b : bool, Equity b o) ->
 Exists (in_SC false)
   (protocol (proc false (proc false (proc false initial))) o).
 SolveSimpleNode.
apply fntt2; [ auto with bool core | apply (cf false true diff_true_false) ].
Qed.
Hint Resolve fnfff2.

(***************************************************************
  The soundness theorem asserts that each of the processes will
   always enter into the critical section once more.
 ***************************************************************)

Definition Soundness (m : Memo) :=
  forall o : Oracle,
  (forall b : bool, Equity b o) ->
  forall id : bool, ForAll (Exists (in_SC id)) (choix proc m o).

Theorem soundness : Soundness initial.
cofix soundness_initial with (soundness_st : Soundness (proc true initial))
 (soundness_stt : Soundness (proc true (proc true initial)))
 (soundness_stf : Soundness (proc false (proc true initial)))
 (soundness_sttf : Soundness (proc false (proc true (proc true initial))))
 (soundness_sf : Soundness (proc false initial))
 (soundness_sft : Soundness (proc true (proc false initial)))
 (soundness_sff : Soundness (proc false (proc false initial)))
 (soundness_sfft : Soundness (proc true (proc false (proc false initial))))
 (soundness_sfff : Soundness (proc false (proc false (proc false initial))));
 (unfold Soundness in soundness_stf; unfold Soundness in soundness_sttf;
   unfold Soundness in soundness_sf; unfold Soundness in soundness_sft;
   unfold Soundness in soundness_sff; unfold Soundness in soundness_sfft;
   unfold Soundness in soundness_sfff; unfold Soundness in soundness_initial;
   unfold Soundness in soundness_st; unfold Soundness in soundness_stt;
   unfold Soundness in |- *; simple destruct id);
 (constructor;
   [ auto with bool core
   | simpl in |- *; case (hd o); (simpl in |- *; auto with bool core) ]).
Qed.

repo: mutual-exclusion


text:
From Undecidability.L.Tactics Require Import LTactics GenEncode.
From Undecidability.L.Datatypes Require Import Lists LProd LNat.
From Undecidability.L.Functions Require Import EqBool.

From Complexity.Complexity Require Import NP Definitions PolyTimeComputable.
From Complexity.Libs.CookPrelim Require Import Tactics.

From Complexity.NP Require Import SharedSAT SAT SAT_inNP.

(** * Comparison of techniques for deriving resource bounds we explored *)

(**
  Roughly, the following techniques are used at some stages of the Cook-Levin proof:
  - Explicit Bounds: solve the recurrence explicitly, factoring constants into definitions, and then directly derive a polynomial bound.
      This approach is quite simple and therefore is applicable in pretty much all cases, but is very verbose and not very elegant.
    This technique was used for the chain of reductions of SingleTMGenNP to SAT.

  - Intuitive Bounds using pure upToC: This uses the upToC mechanism to elegantly abstract from constants and phrases bounds in terms of abstract size functions.
    This technique was used for large parts of the L to TMGenNP reduction.

  - Intuitive Bounds with upToC, reverting to abstract functions when bounds become too complicated:
      The previous approach phrases all bounds explicitly. Instead we can also use the running-time functions of component functions as blackboxes in case unfolding them would become too complicated (this can be the case with many nested recursions).
    This technique was used for the SAT verifier used in the NP containment proof.

  - Abstract polyTimeComputable bounds:
      This approach relies on compositionally applying polyTimeComputable proofs for functions to achieve a proof of polynomial-time computability, instead of deriving explicit, more accurate bounds.
      Inherently, this relies on writing functions in combinator style (i.e. without explicit lets/fixes/lambdas), although an extension to this would be imaginable with sufficient automation.
      For functions where this approach is applicable, proofs can become very short and compositonal (for others, not so much).
    This technique was used for the reduction from the abstract heap machine to Turing machines (LM_to_mTM).

  Below, we evaluate the first three techniques on the SAT verifier.
*)

(** * Explicit Bounds *)
(**
  This is the simplest possible approach.
  We just write down the recurrences directly and then derive a polynomial bound.
*)

From Complexity.Complexity Require UpToCPoly.
From Complexity.Libs Require CookPrelim.PolyBounds.

Module explicit_bounds.
Section explicit_bounds.
  Import Lists.
  Import Complexity.Libs.CookPrelim.PolyBounds.
  Import SAT.

  (** extraction of list_in_decb *)
  Section fixXeq.
    Variable (X : Type).
    Context {H : encodable X}.

    Context (eqbX : X -> X -> bool).
    Context {Xeq : eqbClass eqbX}.
    Context {XeqbComp : eqbCompT X}.

    Definition c__listInDecb := 21.
    Fixpoint list_in_decb_time (l : list X) (e : X) :=
      match l with
      | [] => c__listInDecb
      | x :: l => eqbTime (X := X) (size (enc x)) (size (enc e)) + c__listInDecb + list_in_decb_time l e
      end.
#[export]
Instance term_list_in_decb : computableTime' (@list_in_decb X eqbX) (fun l _ => (5, fun x _ => (list_in_decb_time l x, tt))).
    Proof.  extract. solverec.  all: unfold c__listInDecb; solverec. Qed.
  End fixXeq.
#[export]
Existing Instance term_list_in_decb.

  Definition TODO {Y:Type} : Y. Admitted.

  Notation ntodo := (TODO (Y := nat)).

  (** extraction of evalVar *)
  Definition c__evalVar := 6.
  Definition evalVar_time (a : assgn) (v : var) := list_in_decb_time a v + c__evalVar.
#[export]
Instance term_evalVar : computableTime' evalVar (fun a _ => (1, fun v _ => (evalVar_time a v, tt))).
  Proof. extract. solverec. unfold evalVar_time, c__evalVar; solverec. Qed.

  (* One would really like to do this all nicer, in one single record.
    However, that way we couldn't nicely deal with cascaded functions... *)
  Definition poly__evalVar (n : nat) := (n+1) * (c__eqbComp nat + c__listInDecb + c__evalVar + 1).
  Lemma evalVar_time_bound a v : evalVar_time a v <= poly__evalVar (size (enc a)).
  Proof.
    induction a as [ | v0 a IH]; unfold evalVar_time; solverec; cycle 1.
    { rewrite eqbTime_le_l. unfold evalVar_time in IH. rewrite <- !Nat.add_assoc. rewrite IH.
      unfold poly__evalVar. rewrite size_list_cons.
      unfold c__listsizeCons. lia.
    }
    unfold poly__evalVar. solverec.
  Qed.
  Lemma evalVar_poly : inOPoly poly__evalVar /\ monotonic poly__evalVar.
  Proof. unfold poly__evalVar; split; smpl_inO. Qed.
  Smpl Add apply evalVar_poly : inO.

  (** evalLiteral *)
  Definition c__evalLiteral := c__eqbBool + 7.
  Definition evalLiteral_time (a : assgn) (l : literal) :=
    match l with | (s, v) => evalVar_time a v + c__evalLiteral end.
#[export]
Instance term_evalLiteral : computableTime' evalLiteral (fun a _ => (1, fun l _ => (evalLiteral_time a l, tt))).
  Proof. extract. solverec. unfold c__evalLiteral; lia. Qed.

  Implicit Type (n : nat).
  Definition poly__evalLiteral n := poly__evalVar n + c__evalLiteral.
  Lemma evalLiteral_time_bound a l : evalLiteral_time a l <= poly__evalLiteral (size (enc a)).
  Proof.
    unfold evalLiteral_time. destruct l as [s v]. rewrite evalVar_time_bound.
    unfold poly__evalLiteral; solverec.
  Qed.
  Lemma evalLiteral_poly : inOPoly poly__evalLiteral /\ monotonic poly__evalLiteral.
  Proof. unfold poly__evalLiteral; split; smpl_inO. Qed.
  Smpl Add apply evalLiteral_poly : inO.

  Section fixX.
    Context {X : Type} `{encodable X}.

    (* existsb *)
    Definition c__existsb := 15.
    Fixpoint existsb_time (fT : X -> nat) (l : list X) :=
      match l with
      | [] => c__existsb
      | h :: l' => c__existsb + fT h + existsb_time fT l'
      end.
#[export]
Instance term_existsb : computableTime' (@existsb X) (fun f fT => (1, fun l _ => (existsb_time (callTime fT) l, tt))).
    Proof. extract. solverec; unfold c__existsb; solverec. Qed.

    (* forallb *)
    Definition c__forallb := 15.
    Fixpoint forallb_time (fT : X -> nat) (l : list X) :=
      match l with
      | [] => c__forallb
      | h :: l' => c__forallb + fT h + forallb_time fT l'
      end.
#[export]
Instance term_forallb : computableTime' (@forallb X) (fun f fT => (1, fun l _ => (forallb_time (callTime fT) l, tt))).
    Proof. extract. solverec; unfold c__forallb; solverec. Qed.
  End fixX.
#[export]
Existing Instances term_forallb term_existsb.

  Implicit Types (a : assgn) (C : clause) (N : cnf).

  (* evalClause *)
  Definition c__evalClause := 3.
  Definition evalClause_time a C := existsb_time (evalLiteral_time a) C + c__evalClause.
#[export]
Instance term_evalClause : computableTime' evalClause (fun a _ => (1, fun C _ => (evalClause_time a C, tt))).
  Proof. extract. solverec. unfold evalClause_time, c__evalClause; simp_comp_arith; solverec. Qed.

  Lemma existsb_time_explicit {X : Type} fT (l : list X) : existsb_time fT l <= sumn (map fT l) + (|l| + 1) * c__existsb.
  Proof. induction l as [ | h l IH]; solverec. Qed.

  Definition poly__evalClause n := n * poly__evalLiteral n + (n + 1) * c__existsb + c__evalClause.
  Lemma evalClause_time_bound a C : evalClause_time a C <= poly__evalClause (size (enc a) + size (enc C)).
  Proof.
    unfold evalClause_time. rewrite existsb_time_explicit.
    rewrite sumn_map_mono. 2:{ intros. rewrite evalLiteral_time_bound at 1. instantiate (1 := fun _ => _); cbn; reflexivity. }
    rewrite sumn_map_const. rewrite list_size_length.
    poly_mono evalLiteral_poly. 2: replace_le (size (enc a)) with (size (enc a) + size (enc C)) by lia at 1; reflexivity.
    unfold poly__evalClause; lia.
  Qed.
  Lemma evalClause_poly : monotonic poly__evalClause /\ inOPoly poly__evalClause.
  Proof. unfold poly__evalClause; split; smpl_inO. Qed.
  Smpl Add apply evalClause_poly : inO.

  (* evalCnf *)
  Definition c__evalCnf := 3.
  Definition evalCnf_time a N := forallb_time (evalClause_time a) N + c__evalCnf.
#[export]
Instance term_evalCnf : computableTime' evalCnf (fun a _ => (1, fun N _ => (evalCnf_time a N, tt))).
  Proof. extract. solverec. unfold evalCnf_time, c__evalCnf; simp_comp_arith; solverec. Qed.

  Lemma forallb_time_explicit {X : Type} fT (l : list X) : forallb_time fT l <= sumn (map fT l) + (|l| + 1) * c__forallb.
  Proof. induction l as [ | h l IH]; solverec. Qed.

  Definition poly__evalCnf n := n * poly__evalClause n + (n + 1) * c__forallb + c__evalCnf.
  Lemma evalCnf_time_bound a N : evalCnf_time a N <= poly__evalCnf (size (enc a) + size (enc N)).
  Proof.
    unfold evalCnf_time. rewrite forallb_time_explicit.
    rewrite sumn_map_mono. 2:{ intros. rewrite evalClause_time_bound at 1.
      poly_mono evalClause_poly at 1. 2: { rewrite list_el_size_bound with (a := x). 2: apply H. reflexivity. }
      instantiate (1 := fun _ => _); cbn; reflexivity. }
    rewrite sumn_map_const. rewrite list_size_length.
    unfold poly__evalCnf; lia.
  Qed.
  Lemma evalCnf_poly : monotonic poly__evalCnf /\ inOPoly poly__evalCnf.
  Proof. unfold poly__evalCnf; split; smpl_inO. Qed.
  Smpl Add apply evalCnf_poly : inO.

  (** sat_verifierb *)
  Definition c__satVerifierb := 6.
  Definition sat_verifierb_time (p : cnf * assgn) := let (N, a) := p in evalCnf_time a N + c__satVerifierb.
#[export]
Instance term_sat_verifierb : computableTime' sat_verifierb (fun p _ => (sat_verifierb_time p, tt)).
  Proof. extract. solverec. unfold c__satVerifierb; solverec. Qed.

  Definition poly__satVerifierb n := poly__evalCnf n + c__satVerifierb.
  Lemma sat_verifierb_time_bound p : sat_verifierb_time p <= poly__satVerifierb (size (enc p)).
  Proof.
    unfold sat_verifierb_time, poly__satVerifierb.
    destruct p as [N a]. rewrite evalCnf_time_bound.
    poly_mono evalCnf_poly. 2: { instantiate (1 := size (enc (N, a))). rewrite size_prod; cbn; lia. }
    lia.
  Qed.
  Lemma sat_verifierb_poly : inOPoly poly__satVerifierb /\ monotonic poly__satVerifierb.
  Proof. unfold poly__satVerifierb; split; smpl_inO. Qed.

  (** We obtain that SAT is in NP *)
  Import NP.
  Lemma sat_NP : inNP SAT.
  Proof.
    apply inNP_intro with (R:= sat_verifier).
    1 : apply linDec_polyTimeComputable.
    2 : {
      exists (fun n => n * (1 + c__listsizeCons + c__listsizeNil)).
      3, 4: smpl_inO.
      - unfold SAT, sat_verifier.
        intros cn  a H.  cbn. exists a; tauto.
      - unfold SAT, sat_verifier. intros cn [a H]. exists (compressAssignment a cn). split.
        + apply compressAssignment_cnf_equiv in H. cbn. apply H.
        + apply assignment_small_size. cbn. apply compressAssignment_small.
    }

    unfold inTimePoly. exists poly__satVerifierb. repeat split.
    { exists (sat_verifierb).
      + eexists. eapply computesTime_timeLeq. 2: apply term_sat_verifierb.
        cbn. intros [N a] _. split; [ | easy]. apply sat_verifierb_time_bound.
      + intros [N a]. cbn. apply sat_verifierb_correct.
    }
    all: apply sat_verifierb_poly.
  Qed.
End explicit_bounds.
End explicit_bounds.

(** * Intuitive Bounds using upToC *)
(** We use the upToC mechanism to hide constants.
  This enables us to nicely solve recurrences explicitly to get _closed_ running time functions which are quite close to analyses on paper. *)
Import UpToCPoly.

Module uptoc_pure.
Section uptoc_pure.
  Section fixXeq.
    Variable (X : Type).
    Context {H : encodable X}.

    (** An abstract size function giving the element of l with the maximum encoding size. In practice, we will instantiate it with nat below *)
    Definition maxSize (l : list X) := maxl (map (fun x => size (enc x)) l).
    Lemma maxSize_enc_size (l : list X) : maxSize l<= size (enc l).
    Proof.
      unfold maxSize. rewrite maxl_leq_l.
      2: { intros n (x & <- & Hel)%in_map_iff. apply list_el_size_bound, Hel. }
      easy.
    Qed.

    Context (eqbX : X -> X -> bool).
    Context {Xeq : eqbClass eqbX}.
    Context {XeqbComp : eqbCompT X}.

    Definition list_in_decb_time (L : list X) := ((|L|) + 1) * (maxSize L + 1) + 1.
    Fact _term_list_in_decb : { time : UpToC list_in_decb_time & computableTime' (@list_in_decb X eqbX) (fun L _ => (5, fun e _ => (time L, tt))) }.
    Proof using XeqbComp Xeq.
      exists_const c.
      { extract. solverec; cycle 1.
        + unfold eqbTime. rewrite Nat.le_min_l.
          unfold list_in_decb_time.
          pose (g := max (size (enc x)) (maxSize l)).
          replace_le (size (enc x)) with g by (subst g; apply Nat.le_max_l) at 1.
          replace_le (maxSize l) with g by (subst g; apply Nat.le_max_r) at 1.
          cbn. fold (maxSize l) g.
          instantiate (c := c__eqbComp X + 21). subst c. lia.
        + subst c. unfold list_in_decb_time. cbn. lia. }
      smpl_upToC_solve.
    Qed.
#[export]
Instance term_list_in_decb : computableTime' (@list_in_decb X eqbX) _ := projT2 _term_list_in_decb.
  End fixXeq.
#[export]
Existing Instance term_list_in_decb.

  (** extraction of evalVar *)
  (* evalVar *)
  Definition evalVar_time (a : assgn) := ((|a|) + 1) * (maxSize a + 1).
  Fact _term_evalVar : { time : UpToC evalVar_time & computableTime' evalVar (fun a _ => (1, fun v _ => (time a, tt))) }.
  Proof.
    exists_const c1.
    { extract. solverec. erewrite !UpToC_le. unfold list_in_decb_time. set_consts.
      unfold evalVar_time. inst c1 with (2*C + 6). lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalVar : computableTime' evalVar _ := projT2 _term_evalVar.

  (* evalLiteral*)
  Definition evalLiteral_time (a : assgn) := ((|a|) + 1) * (maxSize a + 1).
  Fact _term_evalLiteral : {time : UpToC evalLiteral_time & computableTime' evalLiteral (fun a _ => (1, fun l _ => (time a, tt)))}.
  Proof.
    exists_const c1.
    { extract. solverec. erewrite !UpToC_le. unfold evalVar_time.
      set_consts. unfold evalLiteral_time. inst c1 with (C + c__eqbBool + 7). lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalLiteral : computableTime' evalLiteral _ := projT2 _term_evalLiteral.

  (* existsb *)
  Definition existsb_time {X : Type} `{encodable X} (p : (X -> nat) * list X) := let '(fT, l) := p in
    sumn (map fT l) + |l| + 1.
  Fact _term_existsb (X : Type) `{encodable X} : { time : UpToC existsb_time & computableTime' (existsb (A := X)) (fun f fT => (1, fun L _ => (time (callTime fT, L), tt)))}.
  Proof.
    exists_const c1.
    { extract. solverec; cycle 1. instantiate (c1 := 15). all: lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_existsb (X : Type) `{encodable X} : computableTime' (@existsb X) _ := projT2 _term_existsb.

  (* forallb *)
  Definition forallb_time {X : Type} `{encodable X} (p : (X -> nat) * list X) := let '(fT, l) := p in
    sumn (map fT l) + |l| + 1.
  Fact _term_forallb (X : Type) `{encodable X} : { time : UpToC forallb_time & computableTime' (forallb (A := X)) (fun f fT => (1, fun L _ => (time (callTime fT, L), tt)))}.
  Proof.
    exists_const c1.
    { extract. solverec; cycle 1. instantiate (c1 := 15). all: lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_forallb (X : Type) `{encodable X} : computableTime' (@forallb X) _ := projT2 _term_forallb.

  (* evalClause *)
  Definition evalClause_time (p : assgn * clause) := let (a, C) := p in (|C| + 1) * ((|a|) + 1) * (maxSize a + 1).
  Fact _term_evalClause : { time : UpToC evalClause_time & computableTime' evalClause (fun a _ => (5, fun C _ => (time (a, C), tt))) }.
  Proof.
    exists_const c1.
    { extract. recRel_prettify2; cycle 1. cbn. 2: lia.
      rewrite !UpToC_le. unfold existsb_time.
      setoid_rewrite sumn_map_mono. 2: { intros. rewrite !UpToC_le at 1. inst_const. }
      unfold evalLiteral_time. rewrite sumn_map_const. set_consts.
      inst c1 with (C + 2*C * C0 + 3). lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalClause : computableTime' evalClause _ := projT2 _term_evalClause.

  Lemma sumn_map_mult_c_l (X : Type) (f : X -> nat) (c : nat) (l : list X):
    sumn (map (fun x : X => c * f x) l) = c * sumn (map f l).
  Proof. induction l; cbn; lia. Qed.

  (* evalCnf *)
  (* essentially, we inline the rt function of evalClause here -- that doesn't seem very nice*)
  Definition evalCnf_time (p : assgn * cnf) := let (a, N) := p in
    sumn (map (fun C => (|C| + 1) ) N) * ((|a|) + 1) * (maxSize a + 1) + (|N|) + 1.
  Fact _term_evalCnf : { time : UpToC evalCnf_time & computableTime' evalCnf (fun a _ => (1, fun N _ => (time (a, N), tt)))}.
  Proof.
    exists_const c1.
    { extract.
      recRel_prettify2. lia.
      cbn. rewrite UpToC_le. cbn.
      unfold forallb_time. rewrite sumn_map_mono. 2: { intros. rewrite UpToC_le at 1. inst_const. }
      rewrite sumn_map_mult_c_l. do 2 rewrite sumn_map_mult_c_r. set (sumn _).
      set_consts. inst c1 with ((C+1) * (C0 +1) +7). lia.
    }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalCnf : computableTime' evalCnf _ := projT2 _term_evalCnf.
  Arguments evalCnf_time : simpl never.

  (** sat_verifierb *)
  Definition sat_verifierb_time (p : cnf * assgn) : nat := let '(N, a) := p in
    sumn (map (fun C => (|C| + 1) ) N) * ((|a|) + 1) * (maxSize a + 1) + (|N|) + 1.
  Fact _term_sat_verifierb : { time : UpToC sat_verifierb_time & computableTime' sat_verifierb (fun p _ => (time p, tt))}.
  Proof.
    exists_const c1.
    { extract. recRel_prettify2. cbn. rewrite UpToC_le. unfold evalCnf_time.
      set_consts. inst c1 with (C + 6). lia.
    }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_sat_verifierb : computableTime' sat_verifierb _ := projT2 _term_sat_verifierb.

  (** We obtain that SAT is in NP *)
  Import NP.
  Lemma sat_NP : inNP SAT.
  Proof.
    apply inNP_intro with (R:= sat_verifier).
    1 : apply linDec_polyTimeComputable.
    2 : {
      exists (fun n => n * (1 + c__listsizeCons + c__listsizeNil)).
      3, 4: smpl_inO.
      - unfold SAT, sat_verifier.
        intros cn a H.  cbn. exists a; tauto.
      - unfold SAT, sat_verifier. intros cn [a H]. exists (compressAssignment a cn). split.
        + apply compressAssignment_cnf_equiv in H. cbn. apply H.
        + apply assignment_small_size. cbn. apply compressAssignment_small.
    }

    unfold inTimePoly. exists_poly p. repeat split.
    { exists (sat_verifierb).
      + eexists. eapply computesTime_timeLeq. 2: apply term_sat_verifierb.
        cbn. intros [N a] _. split; [ | easy]. rewrite !UpToC_le. unfold sat_verifierb_time.
        rewrite sumn_map_mono. 2: { intros. rewrite list_size_length at 1. rewrite list_el_size_bound at 1. 2: apply H. inst_const. }
        rewrite sumn_map_const.
        rewrite !list_size_length. rewrite maxSize_enc_size.
        replace_le (size (enc N)) with (size (enc (N, a))); cycle 1.
        replace_le (size (enc a)) with (size (enc (N, a))); cycle 1.
        [p]: intros n. set (size (enc _)). and_solve p.
        all: rewrite size_prod; cbn; lia.
      + intros [N a]. cbn. apply sat_verifierb_correct.
    }
    all: subst p; smpl_inO.
  Qed.
End uptoc_pure.
End uptoc_pure.

(** * A mixed approach  (this is the one currently used in the SAT file) *)
(** as soon as an intuitive bound becomes ugly and we'd need to use it to bound another function,
  we instead first prove a polynomial bound and save us the effort of deriving an "exact" (up to constants) bound *)
Module uptoc_mixed.
Section uptoc_mixed.
  (** extraction of list_in_decb *)
  Section fixXeq.
    Variable (X : Type).
    Context {H : encodable X}.

    Context (eqbX : X -> X -> bool).
    Context {Xeq : eqbClass eqbX}.
    Context {XeqbComp : eqbCompT X}.

    Definition list_in_decb_time (L : list X) := ((|L|) + 1) * (maxSize L + 1) + 1.
    Fact _term_list_in_decb : { time : UpToC list_in_decb_time & computableTime' (@list_in_decb X eqbX) (fun L _ => (5, fun e _ => (time L, tt))) }.
    Proof using XeqbComp Xeq.
      exists_const c.
      { extract. solverec; cycle 1.
        + unfold eqbTime. rewrite Nat.le_min_l.
          unfold list_in_decb_time.
          pose (g := max (size (enc x)) (maxSize l)).
          replace_le (size (enc x)) with g by (subst g; apply Nat.le_max_l) at 1.
          replace_le (maxSize l) with g by (subst g; apply Nat.le_max_r) at 1.
          cbn. fold (maxSize l) g.
          inst c with (c__eqbComp X + 21). lia.
        + subst c. unfold list_in_decb_time. cbn. lia. }
      smpl_upToC_solve.
    Qed.
#[export]
Instance term_list_in_decb : computableTime' (@list_in_decb X eqbX) _ := projT2 _term_list_in_decb.
  End fixXeq.
  Local Existing Instance term_list_in_decb.

  (** extraction of evalVar *)
  (* evalVar *)
  Definition evalVar_time (a : assgn) := ((|a|) + 1) * (maxSize a + 1) + 1.
  Fact _term_evalVar : { time : UpToC evalVar_time & computableTime' evalVar (fun a _ => (1, fun v _ => (time a, tt))) }.
  Proof.
    exists_const c1.
    { extract. solverec. erewrite !UpToC_le. unfold list_in_decb_time. set_consts.
      unfold evalVar_time. inst c1 with (C + 6). lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalVar : computableTime' evalVar _ := projT2 _term_evalVar.

  (* evalLiteral*)
  Definition evalLiteral_time (a : assgn) := ((|a|) + 1) * (maxSize a + 1) + 1.
  Fact _term_evalLiteral : {time : UpToC evalLiteral_time & computableTime' evalLiteral (fun a _ => (1, fun l _ => (time a, tt)))}.
  Proof.
    exists_const c1.
    { extract. solverec. erewrite !UpToC_le. unfold evalVar_time.
      set_consts. unfold evalLiteral_time. inst c1 with (C + c__eqbBool + 7). lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalLiteral : computableTime' evalLiteral _ := projT2 _term_evalLiteral.

  (* existsb *)
  Definition existsb_time {X : Type} `{encodable X} (p : (X -> nat) * list X) := let '(fT, l) := p in
    sumn (map fT l) + |l| + 1.
  Fact _term_existsb (X : Type) `{encodable X} : { time : UpToC existsb_time & computableTime' (existsb (A := X)) (fun f fT => (1, fun L _ => (time (callTime fT, L), tt)))}.
  Proof.
    exists_const c1.
    { extract. solverec; cycle 1. instantiate (c1 := 15). all: lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_existsb (X : Type) `{encodable X} : computableTime' (@existsb X) _ := projT2 _term_existsb.

  (* forallb *)
  Definition forallb_time {X : Type} `{encodable X} (p : (X -> nat) * list X) := let '(fT, l) := p in
    sumn (map fT l) + |l| + 1.
  Fact _term_forallb (X : Type) `{encodable X} : { time : UpToC forallb_time & computableTime' (forallb (A := X)) (fun f fT => (1, fun L _ => (time (callTime fT, L), tt)))}.
  Proof.
    exists_const c1.
    { extract. solverec; cycle 1. instantiate (c1 := 15). all: lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_forallb (X : Type) `{encodable X} : computableTime' (@forallb X) _ := projT2 _term_forallb.

  (* evalClause *)
  Definition evalClause_time (p : assgn * clause) := let (a, C) := p in (|C| + 1) * ((|a|) + 1) * (maxSize a + 1).
  Fact _term_evalClause : { time : UpToC evalClause_time & computableTime' evalClause (fun a _ => (5, fun C _ => (time (a, C), tt))) }.
  Proof.
    exists_const c1.
    { extract. recRel_prettify2; cycle 1. cbn. 2: lia.
      rewrite !UpToC_le. unfold existsb_time.
      setoid_rewrite sumn_map_mono. 2: { intros. rewrite !UpToC_le at 1. inst_const. }
      unfold evalLiteral_time. rewrite sumn_map_const. set_consts.
      inst c1 with (C + 2*C * C0 + 3). lia. }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalClause : computableTime' evalClause _ := projT2 _term_evalClause.

  (** Now we notice that the above bound would be quite ugly to use in the evalCnf bound below -- thus we prove a polynomial bound here. *)
  Lemma evalClause_poly : isPoly evalClause_time.
  Proof.
    exists_poly p. [p]: intros n.
    { intros (a & C). unfold evalClause_time.
      rewrite !list_size_length. rewrite maxSize_enc_size.
      rewrite size_prod. cbn. [p] : exact (n * n * n). and_solve p. }
    all: subst p; smpl_inO.
  Qed.
  Arguments evalClause_time: simpl never.

  Lemma sumn_map_mult_c_l (X : Type) (f : X -> nat) (c : nat) (l : list X):
    sumn (map (fun x : X => c * f x) l) = c * sumn (map f l).
  Proof. induction l; cbn; lia. Qed.

  (** evalCnf *)
  (** In evalCnf, now, we use evalClause_time as a primitive, instead of inlining it. *)
  Definition evalCnf_time (p : assgn * cnf) := let (a, N) := p in sumn (map (fun C => evalClause_time (a, C)) N) + (|N|) + 1.
  Fact _term_evalCnf : { time : UpToC evalCnf_time & computableTime' evalCnf (fun a _ => (5, fun N _ => (time (a, N), tt)))}.
  Proof.
    exists_const c1.
    { extract. solverec.
      rewrite UpToC_le.
      unfold forallb_time. rewrite sumn_map_mono. 2: { intros. rewrite UpToC_le at 1. inst_const. }
      rewrite sumn_map_mult_c_l. set (sumn _).
      set_consts. inst c1 with ((C+1) * (C0 +1) +7). lia.
    }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_evalCnf : computableTime' evalCnf _ := projT2 _term_evalCnf.
  Arguments evalCnf_time : simpl never.

  (** again: we would not want to use the above bound explicitly, so we give at least a polynomial bound which can be used. *)
  (** this analysis can compositionally use the evalClause_poly bound *)
  Lemma evalCnf_poly : isPoly evalCnf_time.
  Proof.
    exists_poly p. [p]: intros n.
    { intros (a & N). unfold evalCnf_time. rewrite sumn_map_mono.
      2: { intros x H. rewpoly evalClause_poly at 1. monopoly evalClause_poly at 1.
        2: { instantiate (1 := size (enc (a, N))). rewrite !size_prod; cbn. now rewrite (list_el_size_bound H). }
        inst_const. }
      rewrite sumn_map_const. rewrite list_size_length.
      replace_le (size (enc N)) with (size (enc (a, N))) by rewrite size_prod; cbn; lia.
      set (size _). and_solve p. }
    all: subst p; smpl_inO.
  Qed.

  (** sat_verifierb *)
  Definition sat_verifierb_time (p : cnf * assgn) : nat := let '(N, a) := p in evalCnf_time (a, N) + 1.
  Fact _term_sat_verifierb : { time : UpToC sat_verifierb_time & computableTime' sat_verifierb (fun p _ => (time p, tt))}.
  Proof.
    exists_const c1.
    { extract. solverec.
      rewrite !UpToC_le. set_consts. inst c1 with (C + 10). lia.
    }
    smpl_upToC_solve.
  Qed.
#[export]
Instance term_sat_verifierb : computableTime' sat_verifierb _ := projT2 _term_sat_verifierb.

  (** We obtain that SAT is in NP *)
  Import NP.
  Lemma sat_NP : inNP SAT.
  Proof.
    apply inNP_intro with (R:= sat_verifier).
    1 : apply linDec_polyTimeComputable.
    2 : {
      exists (fun n => n * (1 + c__listsizeCons + c__listsizeNil)).
      3, 4: smpl_inO.
      - unfold SAT, sat_verifier.
        intros cn a H.  cbn. exists a; tauto.
      - unfold SAT, sat_verifier. intros cn [a H]. exists (compressAssignment a cn). split.
        + apply compressAssignment_cnf_equiv in H. cbn. apply H.
        + apply assignment_small_size. cbn. apply compressAssignment_small.
    }

    unfold inTimePoly. exists_poly p. repeat split.
    { exists (sat_verifierb).
      + eexists. eapply computesTime_timeLeq. 2: apply term_sat_verifierb.
        cbn. intros [N a] _. split; [ | easy]. rewrite !UpToC_le. unfold sat_verifierb_time.
        rewpoly evalCnf_poly. monopoly (evalCnf_poly). 2: { instantiate (1 := size (enc (N, a))). rewrite !size_prod. cbn; lia. }
        set (L_facts.size _). [p]: intros n. and_solve p.
      + intros [N a]. cbn. apply sat_verifierb_correct.
    }
    all: subst p; smpl_inO.
  Qed.

End uptoc_mixed.
End uptoc_mixed.

author: uds-psl

repo: coq-library-complexity


text:
(************************************************************************)
(* Copyright (c) 2021, Gergei Bana                                      *)
(*                                                                      *)
(* This work is licensed under the MIT license. The license is          *)
(* described in the file "LICENSE" available at the root of the source  *)
(* or at https://opensource.org/licenses/MIT                            *)
(* Special thanks to Qianli Zhang and Ajay K. Eeralla                   *)
(************************************************************************)

Require Export Coq.Init.Logic.
Require Export Coq.Init.Peano.
Require Export Coq.Arith.EqNat.
Require Export Setoid.
Require Export FunctionalExtensionality.
Require Export Coq.Bool.Bool.
Require Export A_Auxiliaries.

(* For now we set up our logic for shallow embedding *)

(**************************************************************************************)
(**************************************************************************************)
(********************* CCSA SYNTAX WITH SHALLOW EMBEDDING ****************************)
(**************************************************************************************)
(**************************************************************************************)

(**************************************************************************************)
(*************************** FUNCTION SYMBOLS IN GENERAL **************************)
(**************************************************************************************)

(* Our set of function symbols is "Symbols" this set is divided into 5 disjoint groups,
"Deterministic", "Honest", "Adversarial", "Mixed" and "General" symbols, which are further divied into
infinite number of subsets by "Arity". For each "n" natural number we have an arity "narg n"
where "narg" stands for number of arguments. Furthermore, we have a division "arbarg", which stands
for arbitrary arguments, meaning that we do no pre-specify the arity.
  - "Deterministic" function symbols represent computation that does not use randomness
  - "Honest" function symbols represent computation that uses honest randomness only
  - "Adversarial" function symbols represent computation that uses adversarial randomness only
  - "Mixed" function symbols
  - "General" function symbols
 *)
Inductive ComputationType (* set *) : Set :=
| Deterministic
| Honest
| Adversarial
| Mixed
| General.

(* "narg" assignes arity to any natural number whil "arbarg" means arbitrary (unspecified) number of arguments
*)
Inductive arity : Set  :=
|narg : nat -> arity
|arbarg.

(* Our set of function symbols
*)
Inductive Symbols (hag : ComputationType) (arg : arity) :  Set :=
| symbols  : list nat -> Symbols hag arg.

(**************************************************************************************)
(*************************** PREDICATE SYMBOLS IN GENERAL **************************)
(**************************************************************************************)

(* Since we only have the indistinguishability predicate and we do not allow at this point
to add further predicate symbols, we do not need types for predicates similar to what we did for
function symbols. If that were to change, it should be done here. *)

(**************************************************************************************)
(*************************** SPECIFIC FUNCTION SYMBOLS **************************)
(**************************************************************************************)

(* Some specific function symbols *)

(* They could also be just parameters, at least so far we have not used that they are fixed  *)

(* Here the "s" at the end stands for symbol *)

(* constants *)

(* Symbol for identically Error algorithm
*)
Definition defaults : Symbols Deterministic (narg 0) :=
  symbols Deterministic (narg 0) [0].

(* Symbol for identically True algorithm
*)
Definition TRues : Symbols Deterministic (narg 0) :=
  symbols Deterministic (narg 0) [1; 0; 0 ; 1; 1].

(* Symbol for identically False algorithm
*)
Definition FAlses : Symbols Deterministic (narg 0) :=
  symbols Deterministic (narg 0) [1; 0; 0 ; 1; 0].

  (* Non-zero arity function symbols for equality and tests*)

(* Symbol for the algorithm that outputs True when the outputs of the algorithms corresponding to two arguments are equal, False when not equal
*)
Definition EQs : Symbols Deterministic (narg 2) :=
  symbols Deterministic (narg 2) [1; 0; 0 ; 1; 0].

(* Symbol for the algorithm that outputs the output of the algorithm corresponding to the second argument when the output of the algorithm corresponding
to the first arguments is True, outputs the output of the algorithm corresponding to the second argument otherwise.
*)
Definition ITEs : Symbols Deterministic (narg 3) :=
  symbols Deterministic (narg 3) [0].

(*Functions symbols for the adversary. These symbols have no pre-specified number of
arguments*)

Definition  advs (n: nat) : Symbols Adversarial arbarg :=
  symbols Adversarial arbarg [n].

(*************************************** RANDOM BLOCKS ***************************************)

(* nonces stand for disjoint random blocks of the honest tape, each with equal length *)

Definition nonces (n: nat) : Symbols Honest (narg 0) :=
  symbols Honest (narg 0) [n].

author: kmilesz


Require Import Crypto.Specific.Framework.SynthesisFramework.
Require Import Crypto.Specific.solinas32_2e216m2e108m1_10limbs.CurveParameters.

Module P <: PrePackage.
  Definition package : Tag.Context.
  Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined.
End P.

Module Export S := PackageSynthesis P.


text:
Require Import List.

Set Implicit Arguments.

Section Exc_Type.

(* El tipo que representa al codominio de una funci\u00f3n parcial. *)
Inductive exc (V E : Set) : Set :=
  | Value : V -> exc V E
  | Error : E -> exc V E.

Variable V1 V2 V3 E1 E2 : Set.

Definition is_Value (e : exc V1 E1) : Prop :=
  match e with
  | Value _ => True
  | Error _ => False
  end.

End Exc_Type.

(* Descripci\u00f3n sencilla de los mappings, utilizando listas. *)

Notation "'If' c1 'then' c2 'else' c3" :=
  match c1 with
  | left _ => c2
  | right _ => c3
  end (at level 200).

Section Mapping_Definition.

(* El tipo de los \u00edndices para acceder a una entrada de un map *)
Variable index : Set.
Variable index_eq : forall x y : index, {x = y} + {x <> y}.

(* El tipo de la informaci\u00f3n asociada a cada \u00edndice *)
Variable info : Set.

Record item : Set :=
 Item
    (* \u00edndice*)
    {item_index : index;
    (* informaci\u00f3n asociada al \u00edndice *)
    item_info : info
   }.

(* Mappings como listas *)
Definition mapping : Set := list item.

(* Map vac\u00edo  *)
Definition map_empty : mapping := nil.

(* Map add *)
(* Agrega una nueva entrada a un map.
   Si la entrada ya existe, su informacion se redefine. *)

Fixpoint map_add (mp : mapping) (idx : index)
  (inf : info) : mapping :=
  let newit := (Item idx inf) in
  match mp with
  | nil =>  newit :: map_empty
  | it :: mp1 =>
      If index_eq (item_index it) idx
      then newit :: mp1
      else it :: map_add mp1 idx inf
  end.

(* Map apply *)
(* Aplicaci\u00f3n de un map a un \u00edndice para obtener la informaci\u00f3n asociada
a dicho \u00edndice *)

Fixpoint map_apply (mp : mapping)
  (idx : index) : exc info index :=
  match mp with
  | nil => Error info idx
  | it :: mp1 =>
      If index_eq idx (item_index it)
      then Value index (item_info it)
      else map_apply mp1 idx
  end.

(* Map drop *)
(* Elimina una entrada de un map *)
Fixpoint map_drop (mp : mapping)
  (idx : index) : mapping :=
  match mp with
  | nil => nil
  | it :: mp1 =>
      If index_eq idx (item_index it)
      then map_drop mp1 idx
      else it :: map_drop mp1 idx
  end.

(* Observadores *)

Definition map_valid_index (mp : mapping) (idx : index) : Prop :=
  exists it : _, map_apply mp idx = Value index it.

Fixpoint map_valid_index_fix (mp:mapping) (idx:index) : bool :=
  match mp with
    | nil => false
    | it::mp' =>
      If (index_eq (item_index it) idx) then
        true
      else
        map_valid_index_fix mp' idx
  end.

(* Tama\u00f1o de un Map *)
Definition map_size (mp : mapping) : nat := length mp.

End Mapping_Definition.

author: jgalat

repo: CFPTT

save_path: github-repos/coq/jgalat-CFPTT


text:
(** * Standard event types *)

(* begin hide *)
From ITree.Events Require
     State
     Reader
     (* Writer *)
     Exception
     Nondeterminism
     Map
     Concurrency
     Dependent.
(* end hide *)

(** ** State *)

(**
[[
Variant stateE (S : Type) : Type -> Type :=
| Get : stateE S S
| Put : S -> stateE S unit.
]]
 *)

(** ** Reader *)

(**
[[
Variant readerE (R : Type) : Type -> Type :=
| Ask : readerE R R.
]]
 *)

(** ** Writer *)

(**
[[
Variant writerE (W : Type) : Type -> Type :=
| Tell : W -> writerE W unit.
]]
 *)

(** ** Exception *)

(**
[[
Variant exceptE (Err : Type) : Type -> Type :=
| Throw : Err -> exceptE Err void.
]]
 *)

(** ** Nondeterminism *)

(**
[[
Variant nondetE : Type -> Type :=
| Or : nondetE bool.
]]
 *)

(** ** Map *)

(**
[[
Variant mapE (K V : Type) : Type -> Type :=
| Insert : K -> V -> mapE unit
| Lookup : K -> mapE (option V)
| Remove : K -> mapE unit
.
]]
 *)

(** ** Concurrency *)

(**
[[
Inductive spawnE (E : Type -> Type) : Type -> Type :=
| Spawn : itree (spawnE E +' E) unit -> spawnE E unit.
]]
 *)

(** ** Dependent *)

(**
[[
 Variant depE {I : Type} (F : I -> Type) : Type -> Type :=
| Dep (i : I) : depE F (F i).
]]
 *)

author: euisuny


text:
Require Export Logic_J.

Definition relation (X: Type) := X -> X -> Prop.

Definition partial_function {X: Type} (R: relation X) :=
  forall x y1 y2: X, R x y1 -> R x y2 -> y1 = y2.

Theorem next_nat_partial_function:
  partial_function next_nat.
Proof.
  unfold partial_function.
  intros x y1 y2 P Q.
  inversion P.
  inversion Q.
  reflexivity.
Qed.

Theorem le_not_a_partial_function:
  ~(partial_function le).
Proof.
  unfold not. unfold partial_function.
  intros H.
  assert (0 = 1) as Nonsense.
  apply H with 0.
  apply le_n.
  apply le_S. apply le_n.
  inversion Nonsense.
Qed.

(* Theorem total_relation_not_a_partial_function: *)
(*   ~(partial_function total_relation). *)

Definition reflexive {X: Type} (R: relation X) :=
  forall a: X, R a a.

Theorem le_reflexive:
  reflexive le.
Proof.
  unfold reflexive. intros n. apply le_n.
Qed.

Definition transitive {X: Type} (R: relation X) :=
  forall a b c: X, (R a b) -> (R b c) -> (R a c).

Theorem le_trans: transitive le.
Proof.
  unfold transitive.
  intros n m o Hmn Hmo.
  induction Hmo.
  apply Hmn.
  apply le_S. apply IHHmo.
Qed.

Theorem lt_trans:
  transitive lt.
Proof.
  unfold transitive.
  intros n m o Hnm Hmo.
  apply le_S in Hnm.
  apply le_trans with (a := (S n)) (b := (S m)) (c := o).
  apply Hnm.
  apply Hmo.
Qed.

Theorem lt_trans':
  transitive lt.
Proof.
  unfold lt.
  unfold transitive.
  intros n m o Hnm Hmo.
  induction Hmo as [| m' Hm'o].
  + apply lt_S.
    inversion Hnm.
    apply le_n.
    rewrite H0.
    apply Hnm.
  + apply le_S.
    apply IHHm'o.
Qed.

Theorem lt_trans'':
  transitive lt.
Proof.
  unfold lt. unfold transitive.
  intros m n o Hnm Hmo.
  induction o as [| o'].
  + inversion Hmo.
  + apply le_S.
    inversion Hmo.
    rewrite <- H0.
    apply Hnm.
    apply IHo'.
    apply H0.
Qed.

Theorem le_Sn_le: forall n m, S n <= m -> n <= m.
Proof.
  intros n m H. apply le_trans with (S n).
  apply le_S. apply le_n.
  apply H.
Qed.

Definition symmetric {X: Type} (R: relation X) :=
  forall a b: X, (R a b) -> (R b a).

Definition antisymmetric {X: Type} (R: relation X) :=
  forall a b: X, (R a b) -> (R b a) -> a = b.

Definition equivalence {X: Type} (R: relation X) :=
  (reflexive R) /\ (symmetric R) /\ (transitive R).

Definition order {X:Type} (R: relation X) :=
  (reflexive R) /\ (antisymmetric R) /\ (transitive R).

Definition preorder {X: Type} (R: relation X) :=
  (reflexive R) /\ (transitive R).

Inductive clos_refl_trans {A: Type} (R: relation A) : relation A :=
| rt_step : forall x y, R x y -> clos_refl_trans R x y
| rt_refl : forall x, clos_refl_trans R x x
| rt_trans: forall x y z, clos_refl_trans R x y -> clos_refl_trans R y z -> clos_refl_trans R x z.

author: KeenS


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.X25519.C64.Synthesis.

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

Print Assumptions add.