Skip to content

Commit

Permalink
generated raw materials for the paper.
Browse files Browse the repository at this point in the history
  • Loading branch information
@aa755
aa755 committed Jul 6, 2017
1 parent e1f2385 commit 1e682ca
Show file tree
Hide file tree
Showing 4 changed files with 152 additions and 63 deletions.
1 change: 1 addition & 0 deletions PIW.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -737,6 +737,7 @@ Proof using.
assumption.
Qed.

Print Assumptions IWT_R_iso.

Require Import Coq.Logic.JMeq.
Require Import Coq.Program.Equality.
Expand Down
87 changes: 57 additions & 30 deletions examples/paper.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -615,7 +615,7 @@ forall {A:Type} {B : A -> Type}, forall (f g : forall x : A, B x), (forall x, f

Notation π₁ := projT1.

Definition GoodRel :=
Definition IsoRel :=
λ (A A': Set), {A_R : A -> A' -> Prop & (Total A_R) × (OneToOne A_R)}.

Definition TotalHalf {A A' : Set} (A_R: A -> A' -> Prop) : Type := forall (a:A), {a':A' & (A_R a a')}.
Expand All @@ -624,7 +624,7 @@ Definition anyRelPi {A A' :Set} (A_R: A -> A' -> Prop) {B: A -> Set} {B': A' ->
(B_R: forall a a', A_R a a' -> (B a) -> (B' a') -> Prop) (f: forall a, B a) (f': forall a', B' a')
: Prop := forall a a' (a_R: A_R a a'), B_R _ _ a_R (f a) (f' a').

Lemma totalPiHalf: forall {A A' :Set} (A_R: GoodRel A A') {B: A -> Set} {B': A' -> Set}
Lemma totalPiHalf: forall {A A' :Set} (A_R: IsoRel A A') {B: A -> Set} {B': A' -> Set}
(B_R: forall a a', (π₁ A_R) a a' -> (B a) -> (B' a') -> Prop)
(BTot : forall a a' (a_R:(π₁ A_R) a a'), TotalHalf (B_R _ _ a_R)), TotalHalf (anyRelPi (π₁ A_R) B_R).
Proof.
Expand All @@ -641,10 +641,10 @@ Definttion oneSigmaIWT (I A : Set) (B : A -> Set) (AI : A -> I) (BI : forall (a
Lemma inj_pair2: forall (U : Type) (P : U -> Type) (p : U) (x y : P p), existT p x = existT p y -> x = y.
Abort.

Definition mkGoodRel (A A' : Set) (A_R: A -> A' -> Prop) (A_Rtot: Total A_R) (A_Rone: OneToOne A_R) : GoodRel A A'.
Definition mkIsoRel (A A' : Set) (A_R: A -> A' -> Prop) (A_Rtot: Total A_R) (A_Rone: OneToOne A_R) : IsoRel A A'.
Abort.

Definition projRel (A A' : Set) (A_RG : GoodRel A A') : A -> A' -> Prop.
Definition projRel (A A' : Set) (A_RG : IsoRel A A') : A -> A' -> Prop.
Abort.

Inductive Monad : forall (A:Set), Set := ret : Monad nat.
Expand Down Expand Up @@ -705,9 +705,23 @@ Inductive TmKind :=

Variable tmKind: Tm -> TmKind.

Section eval.
Fixpoint evaln (n:nat) (t:Tm): option Tm :=
match n with
| O => None | S n =>
match (tmKind t) with
| evar | elam _ | enum _ => Some t
| eapp f a =>
match evaln n f, evaln n a with
| Some f, Some a =>
match (tmKind f) with
| elam bt => Some (applyBtm bt a)
| _ => None
end
| _,_ => None
end
end
end.

Variable evaln: nat -> Tm -> option Tm.

(* just this would be an example. However, because it is not recursive,
even tauto may be able to prove it. Even if we only show this on paper,
Expand Down Expand Up @@ -735,45 +749,57 @@ match k with | O => True | S k =>
end
end.

End eval.
Definition obseq (tl tr:Tm) := forall (k:nat), obsEq k tl tr.

Fixpoint evaln (n:nat) (t:Tm): option Tm :=
match n with
| O => None | S n =>
match (tmKind t) with
| evar | elam _ | enum _ => Some t
| eapp f a =>
match evaln n f, evaln n a with
| Some f, Some a =>
match (tmKind f) with
| elam bt => Some (applyBtm bt a)
| _ => None
end
| _,_ => None
end
end
end.

Definition comb (A1 A2 :Set) (A_R: GoodRel A1 A2)

Definition comb (A1 A2 :Set) (A_R: IsoRel A1 A2)
(B1: A1 -> Set)
(B2: A2 -> Set)
(B_R: forall a1 a2, π₁ A_R a1 a2 -> GoodRel (B1 a1) (B2 a2)) :
GoodRel (forall a : A1, B1 a) (forall a : A2, B2 a).
(B_R: forall a1 a2, π₁ A_R a1 a2 -> IsoRel (B1 a1) (B2 a2)) :
IsoRel (forall a : A1, B1 a) (forall a : A2, B2 a).
Proof.
exists (fun (f1 : forall a : A1, B1 a) (f2 : forall a : A2, B2 a) =>
forall (a1 : A1) (a2 : A2) (p : π₁ A_R a1 a2), π₁ (B_R a1 a2 p) (f1 a1) (f2 a2)
).
Abort.

Definition GoodProp :=
forall (A1 A2 :Set) (A_R: GoodRel A1 A2)
forall (A1 A2 :Set) (A_R: IsoRel A1 A2)
(B1: A1 -> Prop)
(B2: A2 -> Prop)
(B_R: forall a1 a2, π₁ A_R a1 a2 -> GoodRel (B1 a1) (B2 a2)),
GoodRel (forall a : A1, B1 a) (forall a : A2, B2 a).
(B_R: forall a1 a2, π₁ A_R a1 a2 -> IsoRel (B1 a1) (B2 a2)),
IsoRel (forall a : A1, B1 a) (forall a : A2, B2 a).

End Squiggle4.

Variable TmKindAnyRel
: forall Tm Tm₂ : Set,
(Tm -> Tm₂ -> Prop) ->
forall BTm BTm₂ : Set,
(BTm -> BTm₂ -> Prop) -> TmKind Tm BTm -> TmKind Tm₂ BTm₂ -> Prop.

Definition obseqStrongIsoType :=
forall (Tm Tm₂ : Set) (Tmᵣ : Tm -> Tm₂ -> Prop)
(Tmᵣtot: Total Tmᵣ)
(BTm BTm₂ : Set) (BTmᵣ : BTm -> BTm₂ -> Prop)
(applyBtm : BTm -> Tm -> Tm)
(applyBtm₂ : BTm₂ -> Tm₂ -> Tm₂)
(applyBtmᵣ : forall (b : BTm) (b₂ : BTm₂) (bᵣ: BTmᵣ b b₂)
(a : Tm) (a₂ : Tm₂) (aᵣ : Tmᵣ a a₂),
Tmᵣ (applyBtm b a) (applyBtm₂ b₂ a₂))
(tmKind : Tm -> TmKind Tm BTm)
(tmKind₂ : Tm₂ -> TmKind Tm₂ BTm₂)
(tmKindᵣ : forall (a : Tm) (a₂ : Tm₂) (aᵣ: Tmᵣ a a₂),
TmKindAnyRel Tm Tm₂ Tmᵣ BTm BTm₂ BTmᵣ
(tmKind a)
(tmKind₂ a₂))
(tl : Tm) (tl₂ : Tm₂) (tlᵣ: Tmᵣ tl tl₂)
(tr : Tm) (tr₂ : Tm₂) (trᵣ: Tmᵣ tr tr₂),
IsoRel (obseq Tm BTm applyBtm tmKind tl tr)
(obseq Tm₂ BTm₂ applyBtm₂ tmKind₂ tl₂ tr₂).


Set Universe Polymorphism.

Inductive list@{i} (A : Type@{i}) : Type@{i} :=
Expand All @@ -789,4 +815,5 @@ Fixpoint list_R@{i} (A: Type@{i}) (A₂ : Type@{i}) (A_R : A -> A₂ -> Type@{i}
(l : list@{i} A) (l₂ : list@{i} A₂) : Type@{i} :=
True.

Lemma IsoRel_implies_iff (A B:Prop) (pb : GoodRel A B) : A <-> B.
Lemma IsoRel_implies_iff (A B:Prop) (pb : IsoRel A B) : A <-> B.
Abort.
4 changes: 4 additions & 0 deletions test-suite/iso/IWTS.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,10 @@ Inductive IWT (I A : Set) (B : A -> Set) (AI : A -> I)
IWT I A B AI BI (AI a).

Run TemplateProgram (genParamIndAll [] "Top.IWTS.IWT").

Print Assumptions Top_IWTS_IWT_pmtcty_RR0tot12.
Print Assumptions Top_IWTS_IWT_pmtcty_RR0one12.

Run TemplateProgram (mkIndEnv "indTransEnv" ["Top.IWTS.IWT"]).
Require Import ReflParam.Trecord.
Print Top_IWTS_IWT_pmtcty_RR0_constr_0_tot.
Expand Down
123 changes: 90 additions & 33 deletions test-suite/iso/squiggle5StrongIso.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,40 +20,41 @@ Require Import ReflParam.Trecord.
Require Import ReflParam.unusedVar.
Declare ML Module "myplug".
Section Test.
Variables (A A₂ : Set)
(Ra : A -> A₂ -> Prop)
(pta : TotalHeteroRel Ra)
(B B₂ : Set)
(Rb : B -> B₂ -> Prop)
(ptb : TotalHeteroRel Rb)
(poa : oneToOne Ra)
Variables
(Tm Tm₂ : Set)
(Tmᵣ : Tm -> Tm₂ -> Prop)
(TmᵣTot : TotalHeteroRel Tmᵣ)
(BTm BTm₂ : Set)
(BTmᵣ : BTm -> BTm₂ -> Prop)
(BTmᵣTot : TotalHeteroRel BTmᵣ)
(TmᵣOne : oneToOne Tmᵣ)
.
Check(
fun (pob : oneToOne Rb) =>
let A_R := (@Build_GoodRel allProps _ _ Ra pta poa) in
let B_R := (@Build_GoodRel allProps _ _ Rb ptb pob) in
fun (BTmᵣOne : oneToOne BTmᵣ) =>
let A_R := (@Build_GoodRel allProps _ _ Tmᵣ TmᵣTot TmᵣOne) in
let B_R := (@Build_GoodRel allProps _ _ BTmᵣ BTmᵣTot BTmᵣOne) in
Top_squiggle5_obseq_pmtcty_RR _ _ A_R _ _ B_R
).

Time Detect (
fun (pob : oneToOne Rb) =>
let A_R := (@Build_GoodRel allProps _ _ Ra pta poa) in
let B_R := (@Build_GoodRel allProps _ _ Rb ptb pob) in
Top_squiggle5_obsEq_pmtcty_RR _ _ A_R _ _ B_R
Time Detect(
fun (BTmᵣOne : oneToOne BTmᵣ) =>
let A_R := (@Build_GoodRel allProps _ _ Tmᵣ TmᵣTot TmᵣOne) in
let B_R := (@Build_GoodRel allProps _ _ BTmᵣ BTmᵣTot BTmᵣOne) in
Top_squiggle5_obseq_pmtcty_RR _ _ A_R _ _ B_R
).

Time
ReduceAwayLamVar sthm := (
fun (pob : oneToOne Rb) =>
let A_R := (@Build_GoodRel allProps _ _ Ra pta poa) in
let B_R := (@Build_GoodRel allProps _ _ Rb ptb pob) in
fun (BTmᵣOne : oneToOne BTmᵣ) =>
let A_R := (@Build_GoodRel allProps _ _ Tmᵣ TmᵣTot TmᵣOne) in
let B_R := (@Build_GoodRel allProps _ _ BTmᵣ BTmᵣTot BTmᵣOne) in
Top_squiggle5_obseq_pmtcty_RR _ _ A_R _ _ B_R
).

Check sthm.
Lemma testDefn (pob : oneToOne Rb):
let A_R := (@Build_GoodRel allProps _ _ Ra pta poa) in
let B_R := (@Build_GoodRel allProps _ _ Rb ptb pob) in
Lemma testDefn (BTmᵣOne : oneToOne BTmᵣ):
let A_R := (@Build_GoodRel allProps _ _ Tmᵣ TmᵣTot TmᵣOne) in
let B_R := (@Build_GoodRel allProps _ _ BTmᵣ BTmᵣTot BTmᵣOne) in
JMeq
(Top_squiggle5_obseq_pmtcty_RR _ _ A_R _ _ B_R)
sthm.
Expand All @@ -64,30 +65,30 @@ Qed.
End Test.

Section Test2.
Variables (A A₂ : Set)
(Ra : A -> A₂ -> Prop)
(pta : TotalHeteroRel Ra)
(B B₂ : Set)
(Rb : B -> B₂ -> Prop)
(ptb : TotalHeteroRel Rb).
Variables
(Tm Tm₂ : Set)
(Tmᵣ : Tm -> Tm₂ -> Prop)
(TmᵣTot : TotalHeteroRel Tmᵣ)
(BTm BTm₂ : Set)
(BTmᵣ : BTm -> BTm₂ -> Prop).

Check (
fun (poa : oneToOne Ra) =>
@sthm _ _ Ra pta _ _ Rb poa
fun (poa : oneToOne Tmᵣ) =>
@sthm _ _ Tmᵣ TmᵣTot _ _ BTmᵣ poa
).
Time Detect
(
fun (poa : oneToOne Ra) =>
sthm _ _ Ra pta _ _ Rb poa
fun (poa : oneToOne Tmᵣ) =>
@sthm _ _ Tmᵣ TmᵣTot _ _ BTmᵣ poa
).
(*The first argument may be omitted. The reduced term is:...
Finished transaction in 1.694 secs (1.447u,0.011s) (successful)
*)

Time ReduceAwayLamVar obseqStrongIso :=
(
fun (poa : oneToOne Ra) =>
sthm A A₂ Ra pta B B₂ Rb poa
fun (poa : oneToOne Tmᵣ) =>
@sthm _ _ Tmᵣ TmᵣTot _ _ BTmᵣ poa
).

(*
Expand All @@ -106,6 +107,62 @@ Abort. (* Qed works, but this using Abort because this lemma should not be used,


Check obseqStrongIso.

Check Top_squiggle5_TmKind_pmtcty_RR0.

(* folding definitions and alpha renaming for readability *)
Definition obseqStrongIsoType :=
forall
(Tm Tm₂ : Set) (Tmᵣ : Tm -> Tm₂ -> Prop)
(Tmᵣtot: TotalHeteroRel Tmᵣ)
(BTm BTm₂ : Set) (BTmᵣ : BTm -> BTm₂ -> Prop)
(applyBtm : BTm -> Tm -> Tm) (applyBtm₂ : BTm₂ -> Tm₂ -> Tm₂)
(applyBtmᵣ : forall (b : BTm) (b₂ : BTm₂) (bᵣ: BTmᵣ b b₂)
(a : Tm) (a₂ : Tm₂) (aᵣ : Tmᵣ a a₂), Tmᵣ (applyBtm b a) (applyBtm₂ b₂ a₂))
(tmKind : Tm -> TmKind Tm BTm)
(tmKind₂ : Tm₂ -> TmKind Tm₂ BTm₂)
(tmKindᵣ : forall (a : Tm) (a₂ : Tm₂)
(aᵣ: Tmᵣ a a₂),
Top_squiggle5_TmKind_pmtcty_RR0 Tm Tm₂ Tmᵣ BTm BTm₂ BTmᵣ (tmKind a)
(tmKind₂ a₂))
(tl : Tm) (tl₂ : Tm₂)
(tlᵣ: Tmᵣ tl tl₂)
(tr : Tm) (tr₂ : Tm₂)
(trᵣ: Tmᵣ tr tr₂),
BestRel (obseq Tm BTm applyBtm tmKind tl tr)
(obseq Tm₂ BTm₂ applyBtm₂ tmKind₂ tl₂ tr₂).

Goal JMeq obseqStrongIsoType ltac:(let T:=type of obseqStrongIso in exact T).
reflexivity.
Qed.

Definition obseqWeakIsoType :=
(forall (Tm Tm₂ : Set) (Tm_R : BestRel Tm Tm₂) (BTm BTm₂ : Set)
(BTm_R : BestRel BTm BTm₂) (applyBtm : BTm -> Tm -> Tm)
(applyBtm₂ : BTm₂ -> Tm₂ -> Tm₂),
(forall (a1 : BTm) (a2 : BTm₂),
BestR BTm_R a1 a2 ->
forall (a3 : Tm) (a4 : Tm₂),
BestR Tm_R a3 a4 -> BestR Tm_R (applyBtm a1 a3) (applyBtm₂ a2 a4)) ->
forall (tmKind : Tm -> TmKind Tm BTm) (tmKind₂ : Tm₂ -> TmKind Tm₂ BTm₂),
(forall (a1 : Tm) (a2 : Tm₂),
BestR Tm_R a1 a2 ->
Top_squiggle5_TmKind_pmtcty_RR0 Tm Tm₂ (BestR Tm_R) BTm BTm₂ (BestR BTm_R)
(tmKind a1) (tmKind₂ a2)) ->
forall (tl : Tm) (tl₂ : Tm₂),
BestR Tm_R tl tl₂ ->
forall (tr : Tm) (tr₂ : Tm₂),
BestR Tm_R tr tr₂ ->
BestRel (forall a : nat, obsEq Tm BTm applyBtm tmKind a tl tr)
(forall a : nat, obsEq Tm₂ BTm₂ applyBtm₂ tmKind₂ a tl₂ tr₂)).

Goal False.
let T:=type of Top_squiggle5_obseq_pmtcty_RR in let t:= eval simpl in T in idtac t.
Abort.

Goal JMeq obseqWeakIsoType ltac:(let T:=type of Top_squiggle5_obseq_pmtcty_RR in exact T).
reflexivity.
Qed.
(*
Lemma dependsOnlyOnTotdivergesIff : existsAOneFreeImpl
(Top_squiggle2_divergesIff_pmtcty_RR).
Expand Down

0 comments on commit 1e682ca

Please sign in to comment.