From Undecidability.L.Complexity Require Export UpToC GenericNary.
Require Import smpl.Smpl.
From Coq Require Import Setoid.
From Coq Require Import CRelationClasses CMorphisms.
From Undecidability.Shared.Libs.PSL Require FinTypes.
Local Set Universe Polymorphism.
Lemma leToC_eta X (f g :X -> _) :
(leUpToC f g) = (leUpToC (fun x => f x) (fun x => g x)).
Proof. reflexivity. Qed.
Smpl Add 2 rewrite leToC_eta in *: nary_prepare.
Set Default Proof Using "Type".
Section workaround.
(*This makes the apply_nary tactic and the rewrites with leToC_eta and "=" work *)
Local Generalizable Variables A R eqA B S eqB.
Global Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
Reflexive (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Global Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) :
Symmetric (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Global Instance pointwise_transitive {A} `(transb : Transitive B eqB) :
Transitive (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Global Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
Equivalence (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Instance workaround1 : @subrelation Type (@eq Type) arrow.
Proof. cbv. firstorder congruence. Qed.
Global Instance workaround2 X Y: (subrelation (pointwise_relation X (@eq Y)) (Morphisms.pointwise_relation X eq)).
Proof. firstorder. Qed.
End workaround.
Lemma upToC_add_nary (domain : list Set) F (f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c F
-> Uncurry f2 <=c F
-> Fun' (fun x => App f1 x + App f2 x) <=c F.
Proof.
prove_nary upToC_add.
Qed.
Lemma upToC_max_nary (domain : list Set) F (f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c F
-> Uncurry f2 <=c F
-> Fun' (fun x => max (App f1 x) (App f2 x)) <=c F.
Proof.
prove_nary upToC_max.
Qed.
Lemma upToC_min_nary (domain : list Set) F (f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c F
-> Uncurry f2 <=c F
-> Fun' (fun x => min (App f1 x) (App f2 x)) <=c F.
Proof.
prove_nary upToC_min.
Qed.
Lemma upToC_mul_c_l_nary (domain : list Set)c F (f : Rarrow domain nat):
Uncurry f <=c F
-> Fun' (fun x => c * App f x) <=c F.
Proof.
prove_nary upToC_mul_c_l.
Qed.
Lemma upToC_mul_c_r_nary (domain : list Set) c F (f : Rarrow domain nat):
Uncurry f <=c F -> Fun'(fun x => App f x * c) <=c F.
Proof.
prove_nary upToC_mul_c_r.
Qed.
Lemma upToC_c_nary (domain : list Set) c F:
(fun _ => 1) <=c F ->
Const' domain c <=c F.
Proof.
prove_nary upToC_c.
Qed.
Lemma upToC_S_nary (domain : list Set) F (f : Rarrow domain nat) :
Const' domain 1 <=c F
-> Uncurry f <=c F
-> Fun' (fun x => S (App f x)) <=c F.
Proof.
prove_nary upToC_S.
Qed.
Lemma upToC_mul_nary (domain : list Set) (F1 F2 f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c Uncurry F1
-> Uncurry f2 <=c Uncurry F2
-> Fun' (fun x => App f1 x * App f2 x) <=c Fun' (fun x => App F1 x * App F2 x).
Proof.
prove_nary upToC_mul.
Qed.
Lemma upToC_pow_r_drop_nary domain c f (F : Rarrow domain nat) :
0 < c
-> f <=c Uncurry F
-> f <=c Fun' (fun x => (App F x) ^ c).
Proof.
now prove_nary upToC_pow_r_drop.
Qed.
Lemma upToC_pow_le_compat_nary domain c c' (f f' : Rarrow domain nat) :
0 < c -> c <= c'
-> Uncurry f <=c Uncurry f'
-> Fun' (fun x => (App f x) ^ c) <=c Fun' (fun x => (App f' x) ^ c').
Proof.
now prove_nary upToC_pow_le_compat.
Qed.
(* Applying n-ary leUpToC lemmas *)
Ltac domain_of_prod S :=
let S := constr:(S) in
let S := eval simpl in S in
list_of_tuple S.
Ltac leUpToC_domain G :=
match G with
| @leUpToC ?F _ _ =>
let L := domain_of_prod F in
let L := constr:(L) in
exact (Mk_domain_of_goal L)
end.
#[export] Hint Extern 0 Domain_of_goal => (mk_domain_getter leUpToC_domain) : domain_of_goal.
Smpl Add 6 first [nary simple apply upToC_add_nary | nary simple apply upToC_mul_c_l_nary | nary simple apply upToC_mul_c_r_nary
| nary simple apply upToC_max_nary| nary simple apply upToC_min_nary
| progress (nary simple apply upToC_c_nary) | _applyIfNotConst_nat (nary simple apply upToC_S_nary)] : upToC.
Ltac destruct_pair_rec p :=
lazymatch type of p with
(_*_)%type=> let lhs := fresh "p" in
let x := fresh "x" in
destruct p as [lhs x];destruct_pair_rec lhs
| _ => idtac
end.
Ltac upToC_le_nary_solve :=
let x := fresh "x" in
apply upToC_le;intros x;destruct_pair_rec x; first [nia|lia].
Smpl Add upToC_le_nary_solve : upToC_solve.
Goal
@leUpToC (nat*bool*nat)
(fun '(xxx,y,z) => xxx+2+3*z) (fun '(x,y,z) => x+z+1).
Proof.
smpl_upToC_solve.
Qed.
Goal (fun '(x,y) => S x + 3 + S y) <=c (fun '(x,y) => x+y+1).
Proof.
timeout 20 (smpl_upToC_solve).
Qed.
Goal (fun '(x,y) => 3) <=c (fun '(x,y) => x+y+1).
Proof.
smpl upToC. smpl upToC_solve.
Qed.
Section bla.
Import FinTypes.
Lemma leUpToC_finCases_nary domain (Y:FinTypes.finType) Z__case (cases : forall (y:Y), Z__case y -> Rtuple domain) (f : Rarrow domain nat) (F : Rtuple domain -> nat) :
(forall x, exists y (z : Z__case y), cases y z = x)
-> (forall y, (fun z => App f (cases y z)) <=c (fun z => F (cases y z)))
-> Fun' (fun x => App f x) <=c F.
Proof.
prove_nary leUpToC_finCases.
Qed.
End bla.
Require Import smpl.Smpl.
From Coq Require Import Setoid.
From Coq Require Import CRelationClasses CMorphisms.
From Undecidability.Shared.Libs.PSL Require FinTypes.
Local Set Universe Polymorphism.
Lemma leToC_eta X (f g :X -> _) :
(leUpToC f g) = (leUpToC (fun x => f x) (fun x => g x)).
Proof. reflexivity. Qed.
Smpl Add 2 rewrite leToC_eta in *: nary_prepare.
Set Default Proof Using "Type".
Section workaround.
(*This makes the apply_nary tactic and the rewrites with leToC_eta and "=" work *)
Local Generalizable Variables A R eqA B S eqB.
Global Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
Reflexive (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Global Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) :
Symmetric (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Global Instance pointwise_transitive {A} `(transb : Transitive B eqB) :
Transitive (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Global Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
Equivalence (pointwise_relation A eqB) | 9.
Proof. firstorder. Qed.
Instance workaround1 : @subrelation Type (@eq Type) arrow.
Proof. cbv. firstorder congruence. Qed.
Global Instance workaround2 X Y: (subrelation (pointwise_relation X (@eq Y)) (Morphisms.pointwise_relation X eq)).
Proof. firstorder. Qed.
End workaround.
Lemma upToC_add_nary (domain : list Set) F (f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c F
-> Uncurry f2 <=c F
-> Fun' (fun x => App f1 x + App f2 x) <=c F.
Proof.
prove_nary upToC_add.
Qed.
Lemma upToC_max_nary (domain : list Set) F (f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c F
-> Uncurry f2 <=c F
-> Fun' (fun x => max (App f1 x) (App f2 x)) <=c F.
Proof.
prove_nary upToC_max.
Qed.
Lemma upToC_min_nary (domain : list Set) F (f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c F
-> Uncurry f2 <=c F
-> Fun' (fun x => min (App f1 x) (App f2 x)) <=c F.
Proof.
prove_nary upToC_min.
Qed.
Lemma upToC_mul_c_l_nary (domain : list Set)c F (f : Rarrow domain nat):
Uncurry f <=c F
-> Fun' (fun x => c * App f x) <=c F.
Proof.
prove_nary upToC_mul_c_l.
Qed.
Lemma upToC_mul_c_r_nary (domain : list Set) c F (f : Rarrow domain nat):
Uncurry f <=c F -> Fun'(fun x => App f x * c) <=c F.
Proof.
prove_nary upToC_mul_c_r.
Qed.
Lemma upToC_c_nary (domain : list Set) c F:
(fun _ => 1) <=c F ->
Const' domain c <=c F.
Proof.
prove_nary upToC_c.
Qed.
Lemma upToC_S_nary (domain : list Set) F (f : Rarrow domain nat) :
Const' domain 1 <=c F
-> Uncurry f <=c F
-> Fun' (fun x => S (App f x)) <=c F.
Proof.
prove_nary upToC_S.
Qed.
Lemma upToC_mul_nary (domain : list Set) (F1 F2 f1 f2 : Rarrow domain nat) :
Uncurry f1 <=c Uncurry F1
-> Uncurry f2 <=c Uncurry F2
-> Fun' (fun x => App f1 x * App f2 x) <=c Fun' (fun x => App F1 x * App F2 x).
Proof.
prove_nary upToC_mul.
Qed.
Lemma upToC_pow_r_drop_nary domain c f (F : Rarrow domain nat) :
0 < c
-> f <=c Uncurry F
-> f <=c Fun' (fun x => (App F x) ^ c).
Proof.
now prove_nary upToC_pow_r_drop.
Qed.
Lemma upToC_pow_le_compat_nary domain c c' (f f' : Rarrow domain nat) :
0 < c -> c <= c'
-> Uncurry f <=c Uncurry f'
-> Fun' (fun x => (App f x) ^ c) <=c Fun' (fun x => (App f' x) ^ c').
Proof.
now prove_nary upToC_pow_le_compat.
Qed.
(* Applying n-ary leUpToC lemmas *)
Ltac domain_of_prod S :=
let S := constr:(S) in
let S := eval simpl in S in
list_of_tuple S.
Ltac leUpToC_domain G :=
match G with
| @leUpToC ?F _ _ =>
let L := domain_of_prod F in
let L := constr:(L) in
exact (Mk_domain_of_goal L)
end.
#[export] Hint Extern 0 Domain_of_goal => (mk_domain_getter leUpToC_domain) : domain_of_goal.
Smpl Add 6 first [nary simple apply upToC_add_nary | nary simple apply upToC_mul_c_l_nary | nary simple apply upToC_mul_c_r_nary
| nary simple apply upToC_max_nary| nary simple apply upToC_min_nary
| progress (nary simple apply upToC_c_nary) | _applyIfNotConst_nat (nary simple apply upToC_S_nary)] : upToC.
Ltac destruct_pair_rec p :=
lazymatch type of p with
(_*_)%type=> let lhs := fresh "p" in
let x := fresh "x" in
destruct p as [lhs x];destruct_pair_rec lhs
| _ => idtac
end.
Ltac upToC_le_nary_solve :=
let x := fresh "x" in
apply upToC_le;intros x;destruct_pair_rec x; first [nia|lia].
Smpl Add upToC_le_nary_solve : upToC_solve.
Goal
@leUpToC (nat*bool*nat)
(fun '(xxx,y,z) => xxx+2+3*z) (fun '(x,y,z) => x+z+1).
Proof.
smpl_upToC_solve.
Qed.
Goal (fun '(x,y) => S x + 3 + S y) <=c (fun '(x,y) => x+y+1).
Proof.
timeout 20 (smpl_upToC_solve).
Qed.
Goal (fun '(x,y) => 3) <=c (fun '(x,y) => x+y+1).
Proof.
smpl upToC. smpl upToC_solve.
Qed.
Section bla.
Import FinTypes.
Lemma leUpToC_finCases_nary domain (Y:FinTypes.finType) Z__case (cases : forall (y:Y), Z__case y -> Rtuple domain) (f : Rarrow domain nat) (F : Rtuple domain -> nat) :
(forall x, exists y (z : Z__case y), cases y z = x)
-> (forall y, (fun z => App f (cases y z)) <=c (fun z => F (cases y z)))
-> Fun' (fun x => App f x) <=c F.
Proof.
prove_nary leUpToC_finCases.
Qed.
End bla.