Commit e9e55145 authored by Robbert Krebbers's avatar Robbert Krebbers

Turn iProp into a notation.

This avoids Coq distinguishing iProp and uPred (iResUR _) when it
should not.
parent 3ba59838
Pipeline #2656 passed with stage
in 9 minutes and 3 seconds
......@@ -116,7 +116,7 @@ Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors cofeT.
Definition iResUR (Σ : gFunctors) : ucmraT :=
iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ).
Notation iProp Σ := (uPredC (iResUR Σ)).
Parameter iProp_unfold: {Σ}, iProp Σ -n> iPreProp Σ.
Parameter iProp_fold: {Σ}, iPreProp Σ -n> iProp Σ.
......@@ -134,7 +134,7 @@ Module Export iProp_solution : iProp_solution_sig.
Definition iPreProp (Σ : gFunctors) : cofeT := iProp_result Σ.
Definition iResUR (Σ : gFunctors) : ucmraT :=
iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ).
Notation iProp Σ := (uPredC (iResUR Σ)).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
solution_fold (iProp_result Σ).
......@@ -145,8 +145,6 @@ Module Export iProp_solution : iProp_solution_sig.
Proof. apply solution_fold_unfold. Qed.
End iProp_solution.
Bind Scope uPred_scope with iProp.
(** * Properties of the solution to the recursive domain equation *)
Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
......
  • This commit not only solved Janno's problem in merge request !9 (merged), but also solved an issue in Amin's code. There, during some proofs, we had to change some occurrences of uPred into iProp because both types appeared in the implicit arguments of length, which in turn made omega and lia fail.

    Edited by Robbert
Markdown is supported
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