Commit 30506849 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix a bunch of Coq 8.8 warnings

parent 8c5c85c7
Pipeline #9209 passed with stage
in 13 minutes and 39 seconds
......@@ -132,10 +132,10 @@ Section definitions.
Proof.
unfold al_enabled'.
split.
- revert x e i. cofix.
- revert x e i. cofix COFIX.
intros x e i Hae.
destruct Hae. econstructor; eauto.
- revert x e i. cofix.
- revert x e i. cofix COFIX.
intros x e i Hae.
destruct Hae. econstructor; eauto.
Qed.
......@@ -228,11 +228,11 @@ Section definitions.
Proof.
unfold ae_taken'.
split.
- revert x e i. cofix.
- revert x e i. cofix COFIX.
intros x e i Hae.
destruct Hae. econstructor; eauto.
apply ev_taken_equiv; auto.
- revert x e i. cofix.
- revert x e i. cofix COFIX.
intros x e i Hae.
destruct Hae. econstructor; eauto.
apply ev_taken_equiv; auto.
......@@ -320,11 +320,11 @@ Section definitions.
simpl; auto.
* intros. destruct Hae.
simpl. eapply IHk. eauto.
- revert x e. cofix.
- revert x e. cofix COFIX.
intros x e Hf. destruct e.
econstructor.
* eapply (Hf 0).
* eapply tr2fun_al; eauto.
* eapply COFIX; eauto.
intros k. specialize (Hf (S k)); auto.
Qed.
......@@ -344,11 +344,11 @@ Section definitions.
edestruct IHk as (k'&?&?); eauto.
exists (S k'); split; auto.
omega.
- revert x e. cofix.
- revert x e. cofix COFIX.
intros x e Hf. destruct e. econstructor.
* edestruct (Hf O) as (k'&?&?).
eapply tr2fun_ev. exists k'. eauto.
* eapply tr2fun_al_ev.
* eapply COFIX.
intros k.
edestruct (Hf (S k)) as (k'&?&?).
destruct k' as [| k']; [omega|].
......@@ -404,11 +404,11 @@ Section definitions.
simpl; destruct e;auto.
* intros. destruct Hae.
simpl. eapply IHk. eauto.
- revert x e. cofix.
- revert x e. cofix COFIX.
intros x e Hf. destruct e.
econstructor.
* simpl in Hf. specialize (Hf 0). simpl in Hf. destruct e; auto.
* eapply tr2fun_al_2; eauto.
* eapply COFIX; eauto.
intros k. specialize (Hf (S k)); auto.
Qed.
......@@ -428,11 +428,11 @@ Section definitions.
edestruct IHk as (k'&?&?); eauto.
exists (S k'); split; auto.
omega.
- revert x e. cofix.
- revert x e. cofix COFIX.
intros x e Hf. destruct e. econstructor.
* edestruct (Hf O) as (k'&?&?).
eapply tr2fun_ev_2. exists k'. eauto.
* eapply tr2fun_al_ev_2.
* eapply COFIX.
intros k.
edestruct (Hf (S k)) as (k'&?&?).
destruct k' as [| k']; [omega|].
......@@ -658,7 +658,7 @@ Section definitions.
induction i.
* intros; destruct Heq; auto.
* intros. destruct Heq; eauto.
- revert x e e'. cofix.
- revert x e e'. cofix COFIX.
intros x e e' Hf.
destruct e as [i x y r e].
destruct e' as [i' x y' r' e'].
......@@ -668,7 +668,7 @@ Section definitions.
generalize (Hf 1); intros Hf1; simpl in Hf1.
destruct e, e'. simpl in *.
inversion Hf1. subst. econstructor.
eapply eq_ext_tr2fun. eauto.
eapply COFIX. eauto.
intros. specialize (Hf (S i)); eauto.
Qed.
......@@ -879,12 +879,12 @@ Section cofair.
{x y} (e: trace R1 x) (e': trace R2 y) i,
enabled_reflecting e e' al_enabled e' i al_enabled e i.
Proof.
cofix. intros x y e e' i Hco Hale.
cofix COFIX. intros x y e e' i Hco Hale.
destruct Hco.
inversion Hale; subst.
econstructor.
* auto.
* eapply enabled_reflecting_al_enabled; eauto.
* eapply COFIX; eauto.
existT_eq_elim; subst; auto.
Qed.
......@@ -924,13 +924,13 @@ Section cofair.
{x y} (e: trace R1 x) (e': trace R2 y) i,
co_step e e' ae_taken e i ae_taken e' i.
Proof.
cofix. intros x y e e' i Hco Hae.
cofix COFIX. intros x y e e' i Hco Hae.
destruct Hco.
inversion Hae; repeat (existT_eq_elim; subst).
econstructor.
* eapply co_step_ev_taken; eauto.
econstructor; eauto.
* eapply co_step_ae_taken; eauto.
* eapply COFIX; eauto.
Qed.
Lemma co_se_fair_pres:
......@@ -967,7 +967,7 @@ Section cofair.
co_se e1 e2 co_step e1 e2 enabled_reflecting e1 e2.
Proof.
intros Hcose.
split; revert x1 x2 e1 e2 Hcose; cofix.
split; revert x1 x2 e1 e2 Hcose; cofix COFIX.
- intros. destruct Hcose. econstructor; eauto.
- intros. destruct Hcose. econstructor; eauto.
Qed.
......@@ -1050,7 +1050,7 @@ Section cofair.
( x e, i', ev_estep x e i')
( x e, ae_ev_estep x e).
Proof.
cofix. intros. destruct e; econstructor; [| | eauto]; eauto.
cofix COFIX. intros. destruct e; econstructor; [| | eauto]; eauto.
Qed.
Lemma ae_ev_estep_destr_clean x e:
......@@ -1859,4 +1859,4 @@ simpl. destruct e. simpl in *.
Qed.
End block.
End cofair.
\ No newline at end of file
End cofair.
......@@ -518,8 +518,8 @@ Section proof.
Lemma dual_involutive (p: protocol): p dual (dual p).
Proof.
revert p. cofix; intros p. rewrite (unfold_prot (dual _)).
destruct p; simpl; econstructor; try eapply dual_involutive.
revert p. cofix COFIX; intros p. rewrite (unfold_prot (dual _)).
destruct p; simpl; econstructor; try eapply COFIX.
Qed.
Lemma prot_inv_left_orient Θ p Φ c pl pr s:
......
......@@ -4,6 +4,10 @@ From fri.chan_lang Require Export lang refine_heap_proofmode.
From fri.chan2heap Require Export refine_protocol.
From fri.chan_lang Require Export simple_types substitution.
From fri.heap_lang Require Import lang heap proofmode substitution.
From iris.proofmode Require coq_tactics.
From fri.heap_lang Require notation proofmode.
From fri.chan_lang Require lang derived refine refine_heap refine_heap_proofmode protocol.
Section lr.
Definition Kd := 200%nat.
(* A hack to be able to ignore delay constants during the logical relations argument *)
......@@ -27,10 +31,9 @@ Section lr.
Local Notation cexprC := (leibnizC (chan_lang.expr)).
Local Notation hvalC := (leibnizC (heap_lang.val)).
Local Notation cvalC := (leibnizC (chan_lang.val)).
From iris.proofmode Require Import coq_tactics.
Import uPred.
Import uPred coq_tactics.
(*
Notation ownT := (λ i ec K, ownT i ec K (dK ec)).
*)
......@@ -68,7 +71,7 @@ Section lr.
Definition lift3 (f: typC hvalC cvalC iProp) : typC -n> hvalC -n> cvalC -n> iProp :=
CofeMor(λ x, CofeMor(λ y, CofeMor (λ z, f x y z))).
From fri.heap_lang Require Import notation.
Import heap_lang.notation.
Fixpoint val_equiv_pre
(ve: typC -n> hvalC -n> cvalC -n> iProp)
......@@ -237,7 +240,7 @@ Section lr.
(* At type 2, expr_equiv in empty context implies
safe_refinement using bool_refine *)
From fri.heap_lang Require Import proofmode notation.
Import heap_lang.notation heap_lang.proofmode.
Lemma subst2typ_inv Γ S x ty:
Γ !! x = Some ty
subst2typ S = Γ
......@@ -355,7 +358,7 @@ Section lr.
- inversion 1.
Qed.
From fri.chan_lang Require Export lang derived refine refine_heap refine_heap_proofmode protocol.
Import chan_lang.lang chan_lang.derived chan_lang.refine chan_lang.refine_heap chan_lang.refine_heap_proofmode chan_lang.protocol.
Lemma tac_refine_bind Δ Δ' k t e K K' P:
envs_lookup k Δ = Some (false, ownT t (fill K' e) K (dK K (fill K' e)))
......
......@@ -114,11 +114,11 @@ Instance dual_proper T: Proper ((≡) ==> (≡)) (@dual T).
Proof.
intros p p' Heq.
revert p p' Heq.
cofix. intros p p' Heq.
cofix COFIX. intros p p' Heq.
rewrite (unfold_prot (dual p)).
rewrite (unfold_prot (dual p')).
destruct p, p'; simpl; try inversion Heq; subst;
econstructor; eapply dual_proper; eauto.
econstructor; eapply COFIX; eauto.
Qed.
......
......@@ -3,6 +3,7 @@ From fri.algebra Require Import list frac dec_agree base_logic.
From fri.program_logic Require Export invariants ghost_ownership.
From fri.program_logic Require Import ownership auth.
From iris.proofmode Require Import tactics.
From iris.proofmode Require coq_tactics.
Import uPred.
Definition scheapN : namespace := nroot .@ "scheap".
......@@ -145,8 +146,6 @@ Section heap.
rewrite option_validI excl_validI /op /excl_op //=.
apply affinely_elim.
Qed.
From iris.proofmode Require Import coq_tactics tactics.
Context (d d': nat).
Context (Hd_le: (d Kd)%nat).
......
......@@ -3,6 +3,7 @@ From fri.algebra Require Import base_logic frac dec_agree.
From fri.program_logic Require Export invariants ghost_ownership.
From fri.program_logic Require Import ownership auth.
From iris.proofmode Require Import tactics.
From fri.heap_lang Require wp_tactics heap.
Import uPred.
Definition sheapN : namespace := nroot .@ "sheap".
......@@ -113,7 +114,7 @@ Section heap.
Lemma sheap_mapsto_op_split l q v : l s{q} v ⊣⊢ (l s{q/2} v l s{q/2} v).
Proof. by rewrite sheap_mapsto_op_eq Qp_div_2. Qed.
From fri.heap_lang Require Export wp_tactics heap.
Import heap_lang.wp_tactics heap_lang.heap.
Context (d d': nat).
Context (Hd_le: (d Kd)%nat).
......@@ -589,4 +590,4 @@ Section heap.
split; omega.
Qed.
End heap.
\ No newline at end of file
End heap.
......@@ -2,6 +2,7 @@ From fri.algebra Require Import base_logic.
From fri.heap_lang Require Export lang notation.
From stdpp Require Import gmap stringmap mapset list.
Global Set Bullet Behavior "Strict Subproofs".
From fri.heap_lang Require heap proofmode notation refine_proofmode substitution.
Section lock_reln.
......@@ -138,7 +139,7 @@ Arguments type_trans _ _%E _%E _.
Hint Constructors type_trans.
Section lr.
From fri.heap_lang Require Import heap proofmode notation refine_proofmode.
Import heap proofmode notation refine_proofmode.
Context (dinit : nat) (Σ: gFunctors) (N: namespace).
Context (Hdisj1: N ## heapN).
Context (Hdisj2: N ## sheapN).
......@@ -329,7 +330,7 @@ Section lr.
stuple { styp : typ ; sval : expr; tval : expr }.
Definition subst_ctx := gmap string subst_tuple.
From fri.heap_lang Require Import substitution.
Import substitution.
Definition subst2typ (S: subst_ctx) : typ_ctx := styp <$> S.
Definition subst2s (S: subst_ctx) : subst_map := sval <$> S.
Definition subst2t (S: subst_ctx) : subst_map := tval <$> S.
......@@ -382,7 +383,7 @@ Section lr.
inversion 1.
Qed.
From iris.proofmode Require Import coq_tactics environments.
Import coq_tactics environments.
Lemma tac_refine_bind Δ Δ' k t e K K' P:
envs_lookup k Δ = Some (false, ownT t (fill K' e) K (dK K (fill K' e)))
envs_simple_replace k false (Esnoc Enil k (ownT t e (comp_ectx K K') (dK (comp_ectx K K') e))) Δ
......@@ -1409,4 +1410,4 @@ Qed.
End lr.
End lock_reln.
\ No newline at end of file
End lock_reln.
Require ClassicalEpsilon.
From fri.algebra Require Export irelations.
From fri.prelude Require Import list set_finite_setoid.
From fri.program_logic Require Export hoare.
......@@ -420,7 +421,7 @@ Section bounded_nondet_hom2.
* eapply Forall_app; auto.
Qed.
Require Import ClassicalEpsilon.
Import ClassicalEpsilon.
Lemma trace_wptp_hom2 (tσ: cfg Λ) (e: trace (idx_step) tσ) b:
( n,
......@@ -432,7 +433,7 @@ Section bounded_nondet_hom2.
trace (B_idx_step) (Some b).
Proof.
revert tσ e b.
cofix.
cofix COFIX.
intros tσ e b Hex.
inversion e; subst.
intros.
......@@ -445,7 +446,7 @@ Section bounded_nondet_hom2.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- eapply trace_wptp_hom2; eauto.
- eapply COFIX; eauto.
intros.
destruct (Hwptp (S (S n))) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' n). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
......@@ -470,7 +471,7 @@ Section bounded_nondet_hom2.
co_se_trace _ B_idx_step e (Some b).
Proof.
revert tσ e b.
cofix.
cofix COFIX.
intros tσ e b Hex.
destruct e as [? tσ1 tσ2 ? ]; subst.
assert (idx_step i tσ1 tσ2) as Hi by auto.
......@@ -491,7 +492,7 @@ Section bounded_nondet_hom2.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- eapply trace_wptp_co_se_hom2; eauto.
- eapply COFIX; eauto.
intros.
destruct (Hwptp (S (S n))) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' n). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
......
Require ClassicalEpsilon.
Require Wellfounded.Lexicographic_Product.
From fri.program_logic Require Import language.
From stdpp Require Import set.
From fri.algebra Require Import irelations.
......@@ -80,7 +82,6 @@ Section delayed_lang.
( p', plt p' p minimal p')
delayed_atomic' (of_val v, p).
Require ClassicalEpsilon.
Definition delayed_atomic: delayed_expr bool.
Proof.
intros e.
......@@ -470,7 +471,6 @@ Section delayed_lang.
intros. eapply IH. eapply Hequiv. eauto.
Qed.
Require Wellfounded.Lexicographic_Product.
Lemma pow_plt_wf (n: nat): wf (pow_plt n).
Proof.
induction n.
......
Require Wellfounded.Lexicographic_Product.
From fri.program_logic Require Import language.
From stdpp Require Import set.
From fri.algebra Require Import irelations.
......@@ -389,7 +390,6 @@ Section delayed_lang.
intros. eapply IH. eapply Hequiv. eauto.
Qed.
Require Wellfounded.Lexicographic_Product.
Lemma pow_plt_wf (n: nat): wf (pow_plt n).
Proof.
induction n.
......
......@@ -2,6 +2,8 @@ From fri.algebra Require Import upred dra cmra_tactics.
From fri.program_logic Require Import
language ectx_language wsat refine_raw refine_raw_adequacy hoare ownership.
From iris.proofmode Require Import tactics.
Require fri.program_logic.refine.
From fri.program_logic Require refine.
Import uPred.
......@@ -26,7 +28,6 @@ Context `{refineG Λ Σ (@ectx_lang expr val ectx state sΛ) Kd}.
(* All the other monoids used must have a trivial step relation *)
Require fri.program_logic.refine.
(* Asserts ownership of physical state sσ in source language *)
Definition ownSP (sσ: state) := refine.ownSP _ sσ.
......@@ -134,7 +135,6 @@ Context (PrimDet: ∀ (e: expr) σ e1' σ1' ef1' e2' σ2' ef2',
Context (PrimDec: (e: expr) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ e' σ' ef', prim_step e σ e' σ' ef'}).
From fri.program_logic Require refine.
Lemma ht_equiv_ectx (E: expr) e (sσ: state) σ Φ:
......
......@@ -3,6 +3,8 @@ From fri.program_logic Require Import
language nat_delayed_language ectx_language wsat refine_raw refine_raw_adequacy
hoare ownership.
From iris.proofmode Require Import tactics.
Require fri.program_logic.refine.
From fri.program_logic Require refine.
Import uPred.
......@@ -20,7 +22,6 @@ Context {expr val ectx state} {sΛ : EctxLanguage expr val ectx state}.
Context `{refineG Λ Σ (delayed_lang (ectx_lang expr) Kd Fd) (S Kd * (Kd + 3))}.
Require fri.program_logic.refine.
(* Asserts ownership of physical state sσ in source language *)
Definition ownSP (sσ: delayed_state _) := refine.ownSP _ sσ.
......@@ -274,7 +275,6 @@ Context (PrimDet: ∀ (e: expr) σ e1' σ1' ef1' e2' σ2' ef2',
Context (PrimDec: (e: expr) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ e' σ' ef', prim_step e σ e' σ' ef'}).
From fri.program_logic Require refine.
Lemma ht_equiv_ectx (E: expr) d e (sσ: state) σ Φ:
......
......@@ -432,7 +432,7 @@ Qed.
- intros; apply excluded_middle_informative.
- intros; apply excluded_middle_informative.
- remember (Some x) as mx. revert mx e x Heqmx.
cofix.
cofix COFIX.
intros mx e x.
destruct e as [i mx y Hstep]. intros ->. destruct y as [y|].
* exists y. intros i' Henabled. destruct Henabled as (y'&?).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment