Skip to content

Commit

Permalink
attempt to remove unnecessary axioms
Browse files Browse the repository at this point in the history
  • Loading branch information
HuStmpHrrr committed May 4, 2024
1 parent 2a0e057 commit dc6ccd5
Show file tree
Hide file tree
Showing 3 changed files with 54 additions and 75 deletions.
34 changes: 0 additions & 34 deletions theories/Core/Axioms.v
Original file line number Diff line number Diff line change
@@ -1,39 +1,5 @@
Require Export Coq.Logic.PropExtensionality.
Require Export Coq.Logic.IndefiniteDescription.
Require Export Coq.Logic.FunctionalExtensionality.


Lemma dep_functional_choice :
forall (A : Type) (B : A -> Type) (R: forall a, B a -> Prop),
(forall x : A, exists y : B x, R x y) ->
(exists f : forall x, B x, forall x : A, R x (f x)).
Proof.
intros.
exists (fun x => proj1_sig (constructive_indefinite_description (R x) (H x))).
intro x.
apply (proj2_sig (constructive_indefinite_description (R x) (H x))).
Qed.

Lemma dep_functional_choice_equiv :
forall (A : Type) (B : A -> Type) (R: forall a, B a -> Prop),
(forall x : A, exists y : B x, R x y) <->
(exists f : forall x, B x, forall x : A, R x (f x)).
Proof.
intros; split.
- apply dep_functional_choice.
- firstorder.
Qed.

Lemma functional_choice_equiv :
forall (A B : Type) (R:A->B->Prop),
(forall x : A, exists y : B, R x y) <->
(exists f : A->B, forall x : A, R x (f x)).
Proof.
intros; split.
- apply functional_choice.
- firstorder.
Qed.

Lemma exists_absorption :
forall (A : Type) (P : A -> Prop) (Q : Prop),
(exists x : A, P x) /\ Q <-> (exists x : A, P x /\ Q).
Expand Down
20 changes: 16 additions & 4 deletions theories/Core/Semantic/PER.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
From Coq Require Import Lia PeanoNat Relations.
From Coq Require Import Lia PeanoNat Relations.Relation_Definitions Classes.RelationClasses.
From Equations Require Import Equations.
From Mcltt Require Import Base Domain Evaluate Readback Syntax System.

Expand All @@ -15,6 +15,12 @@ Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
Inductive rel_mod_app (R : relation domain) f a f' a' : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app R f a f' a'.
Arguments mk_rel_mod_app {_ _ _ _ _}.

Class IrrelevantParametrizedPER {A : Type} (IR : relation A) (OR : forall {a b}, IR a b -> relation A) : Prop := {
IPP_irrelevance : forall {a b} (ab ab' : IR a b), OR ab = OR ab';
IPP_sym : forall {a b} (ab : IR a b) (ba : IR b a), forall c d, OR ab c d -> OR ba d c;
IPP_trans : forall {a1 a2 a3} (a12 : IR a1 a2) (a23 : IR a2 a3) (a13 : IR a1 a3), forall b1 b2 b3, OR a12 b1 b2 -> OR a23 b2 b3 -> OR a13 b1 b3;
}.

Definition per_bot : relation domain_ne := fun m n => (forall s, exists L, {{ Rne m in s ↘ L }} /\ {{ Rne n in s ↘ L }}).
Arguments per_bot /.

Expand Down Expand Up @@ -53,6 +59,8 @@ Section Per_univ_elem_core_def.
`{ forall (in_rel : relation domain)
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
(equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel}}),
PER in_rel ->
IrrelevantParametrizedPER in_rel (@out_rel) ->
(forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
rel_mod_eval per_univ_elem_core B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
(forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
Expand All @@ -76,6 +84,8 @@ Section Per_univ_elem_core_def.
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
{{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} ->
motive A A' in_rel ->
PER in_rel ->
IrrelevantParametrizedPER in_rel (@out_rel) ->
(forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
(forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
Expand All @@ -89,8 +99,8 @@ Section Per_univ_elem_core_def.
per_univ_elem_core_strong_ind a b R (per_univ_elem_core_univ lt_j_i eq) := case_U _ _ lt_j_i eq;
per_univ_elem_core_strong_ind a b R per_univ_elem_core_nat := case_nat;
per_univ_elem_core_strong_ind a b R
(per_univ_elem_core_pi in_rel out_rel equiv_a_a' HT HE) :=
case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a')
(per_univ_elem_core_pi in_rel out_rel equiv_a_a' per ipp HT HE) :=
case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a') per ipp
(fun _ _ equiv_c_c' => match HT _ _ equiv_c_c' with
| mk_rel_mod_eval b b' evb evb' Rel =>
mk_rel_mod_eval b b' evb evb' (conj _ (per_univ_elem_core_strong_ind _ _ _ Rel))
Expand Down Expand Up @@ -138,6 +148,8 @@ Section Per_univ_elem_ind_def.
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
{{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} ->
motive i A A' in_rel ->
PER in_rel ->
IrrelevantParametrizedPER in_rel (@out_rel) ->
(forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
(forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
Expand All @@ -156,7 +168,7 @@ Section Per_univ_elem_ind_def.
per_univ_elem_core_strong_ind i _ (motive i)
(fun j j' j_lt_i eq => case_U j j' i j_lt_i eq (fun A B R' H' => per_univ_elem_ind' _ A B R' _))
(case_N i)
(fun A p B A' p' B' in_rel elem_rel out_rel HA IHA HT HE => case_Pi i out_rel _ IHA _ HE)
(fun A p B A' p' B' in_rel elem_rel out_rel HA IHA per ipp HT HE => case_Pi i out_rel _ IHA per ipp _ HE)
(@case_ne i)
a b R H.

Expand Down
75 changes: 38 additions & 37 deletions theories/Core/Semantic/PERLemmas.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
From Coq Require Import Lia PeanoNat Relations ChoiceFacts Program.Equality.
From Coq Require Import Lia PeanoNat Relations.Relation_Definitions RelationClasses Program.Equality.
From Equations Require Import Equations.
From Mcltt Require Import Axioms Base Domain Evaluate EvaluateLemmas LibTactics PER Readback ReadbackLemmas Syntax System.

Expand Down Expand Up @@ -99,14 +99,14 @@ Proof.
subst.
extensionality f.
extensionality f'.
rewrite H1, H8.
rewrite H3, H12.
extensionality c.
extensionality c'.
extensionality equiv_c_c'.
specialize (H0 _ _ equiv_c_c') as [? ? ? ? []].
specialize (H7 _ _ equiv_c_c') as [? ? ? ? ?].
specialize (H2 _ _ equiv_c_c') as [? ? ? ? []].
specialize (H11 _ _ equiv_c_c') as [? ? ? ? ?].
functional_eval_rewrite_clear.
specialize (H4 _ _ _ eq_refl H7).
specialize (H6 _ _ _ eq_refl H11).
congruence.
Qed.

Expand Down Expand Up @@ -136,44 +136,45 @@ Ltac functional_per_univ_elem_rewrite_clear :=

Lemma per_univ_elem_sym : forall i A B R,
per_univ_elem i A B R ->
exists R', per_univ_elem i B A R' /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R' }}).
per_univ_elem i B A R /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R }}).
Proof.
intros. induction H using per_univ_elem_ind; subst.
- exists (per_univ j'). split.
- split.
+ apply per_univ_elem_core_univ'; trivial.
+ intros. split; intros HD; destruct HD.
* specialize (H1 _ _ _ H0).
firstorder.
* specialize (H1 _ _ _ H0).
firstorder.
- exists per_nat. split.
- split.
+ econstructor.
+ intros; split; mauto.
- destruct IHper_univ_elem as [in_rel' [? ?]].
setoid_rewrite rel_mod_eval_simp_ex in H0.
repeat setoid_rewrite dep_functional_choice_equiv in H0.
destruct H0 as [out_rel' ?].
assert (forall a b : domain, in_rel' a b -> in_rel b a) as Hconv by firstorder.
assert (forall a b : domain, in_rel a b -> in_rel' b a) as Hconv' by firstorder.
setoid_rewrite H1.
exists (fun f f' => forall (c c' : domain) (equiv_c_c' : in_rel' c c'), rel_mod_app (out_rel' c' c (Hconv _ _ equiv_c_c')) f c f' c').
- destruct IHper_univ_elem as [? ?].
setoid_rewrite H3.
split.
+ per_univ_elem_econstructor; eauto.
* intros.
destruct (H0 _ _ (Hconv _ _ equiv_c_c')) as [? ? ? ? [? [? ?]]].
econstructor; eauto.
apply H7.
* auto.
intros.
assert (equiv_c'_c : in_rel c' c) by firstorder.
assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
destruct (H2 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
destruct (H2 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
destruct (H2 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
econstructor; eauto.
functional_eval_rewrite_clear.
per_univ_elem_right_irrel_rewrite.
congruence.

+ split; intros.
* destruct (H0 _ _ (Hconv _ _ equiv_c_c')) as [? ? ? ? [? [? ?]]].
specialize (H4 _ _ (Hconv c c' equiv_c_c')) as [].
econstructor; firstorder eauto.
* destruct (H0 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
specialize (H4 _ _ (Hconv' _ _ equiv_c_c')) as [].
econstructor; firstorder eauto.
replace (Hconv c' c (Hconv' c c' equiv_c_c')) with equiv_c_c' in H11 by apply proof_irrelevance.
firstorder.
- exists per_ne. split.
* assert (equiv_c'_c : in_rel c' c) by firstorder.
destruct (H6 _ _ equiv_c'_c) as [? ? ? ? ?].
econstructor; eauto.
eapply IPP_sym; eassumption.

* assert (equiv_c'_c : in_rel c' c) by firstorder.
destruct (H6 _ _ equiv_c'_c) as [? ? ? ? ?].
econstructor; eauto.
eapply IPP_sym; eassumption.
- split.
+ econstructor.
+ intros; split; mauto.
Qed.
Expand All @@ -183,15 +184,15 @@ Lemma per_univ_elem_left_irrel : forall i A B R A' R',
per_univ_elem i A' B R' ->
R = R'.
Proof.
intros * [? []]%per_univ_elem_sym [? []]%per_univ_elem_sym.
per_univ_elem_right_irrel_rewrite.
extensionality a.
extensionality b.
specialize (H0 a b).
specialize (H2 a b).
apply propositional_extensionality; firstorder.
intros.
apply per_univ_elem_sym in H.
apply per_univ_elem_sym in H0.
destruct_all.
eauto using per_univ_elem_right_irrel.
Qed.

(* JH: the code below has not been fixed yet *)

Ltac per_univ_elem_left_irrel_rewrite :=
repeat match goal with
| H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
Expand Down

0 comments on commit dc6ccd5

Please sign in to comment.