Skip to content

Commit

Permalink
and now with fixed Coq code…
Browse files Browse the repository at this point in the history
  • Loading branch information
MevenBertrand committed Jan 23, 2024
1 parent 28e3f3d commit 732eda6
Show file tree
Hide file tree
Showing 4 changed files with 10 additions and 10 deletions.
4 changes: 2 additions & 2 deletions case-studies/kathrin/coq/ARS.v
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,8 @@ Lemma star_img T1 T2 (f : T1 -> T2) (e1 : Rel T1) e2 :
(forall x y, e1 x y -> star e2 (f x) (f y)) ->
(forall x y, star e1 x y -> star e2 (f x) (f y)).
Proof.
intros. induction H0; eauto.
eapply star_trans with (y0 := f y); eauto.
intros ? x y H. induction H; eauto.
eapply star_trans with (y := f y); eauto.
Qed.

Lemma star_hom T1 T2 (f : T1 -> T2) (e1 : Rel T1) (e2 : Rel T2) :
Expand Down
4 changes: 2 additions & 2 deletions case-studies/kathrin/coq/Chapter10/POPLMark1.v
Original file line number Diff line number Diff line change
Expand Up @@ -290,7 +290,7 @@ Proof.
+ intros. asimpl.
unfold funcomp.
rewrite <- H'. now asimpl.
- eapply T_Tapp with (A0 := A⟨sigma⟩) (B0:=ren_ty (upRen_ty_ty sigma) B).
- eapply T_Tapp with (A := A⟨sigma⟩) (B :=ren_ty (upRen_ty_ty sigma) B).
asimpl in IHty.
eapply IHty; eauto.
eapply sub_weak; eauto.
Expand Down Expand Up @@ -324,7 +324,7 @@ Proof.
eapply context_renaming_lemma; eauto.
* intros. now asimpl.
* intros. now asimpl.
- eapply T_Tapp with (A0 := subst_ty sigma A) (B0:=B[up_ty_ty sigma]).
- eapply T_Tapp with (A := subst_ty sigma A) (B :=B[up_ty_ty sigma]).
asimpl in IHty. eapply IHty; eauto.
eapply sub_substitution; eauto.
now asimpl.
Expand Down
6 changes: 3 additions & 3 deletions case-studies/kathrin/coq/Chapter10/POPLMark21.v
Original file line number Diff line number Diff line change
Expand Up @@ -574,7 +574,7 @@ Proof.
unfold funcomp. rewrite <- H. now asimpl.
+ intros. asimpl.
unfold funcomp. rewrite <- H'. now asimpl.
- cbn. eapply T_Tapp with (A0 := A⟨xi⟩) .
- cbn. eapply T_Tapp with (A := A⟨xi⟩) .
Unshelve.
4: exact (ren_ty (upRen_ty_ty xi) B).
eapply IHty; eauto.
Expand All @@ -585,7 +585,7 @@ Proof.
eapply in_map_iff in H6. destruct H6 as ([j A']&?&?). inv H5.
eapply H3; eassumption.
- cbn. econstructor; eauto. now apply in_map.
- cbn. asimpl. apply letpat_ty with (A0 := A⟨xi⟩) (Gamma'0 := Gamma' >> ⟨xi⟩); eauto.
- cbn. asimpl. apply letpat_ty with (A := A⟨xi⟩) (Gamma' := Gamma' >> ⟨xi⟩); eauto.
+ unfold funcomp. substify.
eauto.
+ asimpl. eapply IHty2; eauto.
Expand Down Expand Up @@ -634,7 +634,7 @@ Proof.
eapply context_renaming_lemma; try eapply eq2.
* intros. now asimpl.
* intros. now asimpl.
- eapply T_Tapp with (A0 := subst_ty sigma A) (B0 := B[up_ty_ty sigma]).
- eapply T_Tapp with (A := subst_ty sigma A) (B := B[up_ty_ty sigma]).
asimpl in IHty. eapply IHty; eauto.
eapply sub_substitution; eauto.
now asimpl.
Expand Down
6 changes: 3 additions & 3 deletions case-studies/kathrin/coq/Chapter10/POPLMark22.v
Original file line number Diff line number Diff line change
Expand Up @@ -581,7 +581,7 @@ Proof.
unfold funcomp. rewrite <- H. now asimpl.
+ intros. asimpl.
unfold funcomp. rewrite <- H'. now asimpl.
- cbn. eapply T_Tapp with (A0 := A⟨xi⟩) (B0 := ren_ty (upRen_ty_ty xi) B).
- cbn. eapply T_Tapp with (A := A⟨xi⟩) (B := ren_ty (upRen_ty_ty xi) B).
asimpl in IHty. eapply IHty; eauto.
eapply sub_weak; eauto. now asimpl.
- econstructor; eauto.
Expand All @@ -590,7 +590,7 @@ Proof.
eapply in_map_iff in H6. destruct H6 as ([j A']&?&?). inv H5.
eapply H3; eassumption.
- cbn. econstructor; eauto. now apply in_map.
- cbn. asimpl. apply letpat_ty with (A0 := A⟨xi⟩) (Gamma'0 := Gamma' >> ⟨xi⟩); eauto.
- cbn. asimpl. apply letpat_ty with (A := A⟨xi⟩) (Gamma' := Gamma' >> ⟨xi⟩); eauto.
+ substify.
eauto.
+ asimpl.
Expand Down Expand Up @@ -638,7 +638,7 @@ Proof.
eapply context_renaming_lemma; try eapply eq2.
* intros. now asimpl.
* intros. now asimpl.
- eapply T_Tapp with (A0 := subst_ty sigma A) (B0 := subst_ty (up_ty_ty sigma) B).
- eapply T_Tapp with (A := subst_ty sigma A) (B := subst_ty (up_ty_ty sigma) B).
asimpl in IHty. eapply IHty; eauto.
eapply sub_substitution; eauto.
now asimpl.
Expand Down

0 comments on commit 732eda6

Please sign in to comment.