Blaisorblade

Equalities in Iris

Using Iris involves dealing with a few subtly different equivalence and equality relations, especially among propositions. This document summarizes these relations and the subtle distinctions among them. It does not replace the Iris appendix, nor "Iris from the grounds up", but it expands on how Iris is mapped into Coq, tho we focus on issues affecting equalities.

Blaisorblade

Require Import ssreflect.
(*
Playing with 
https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#type-families
*)

Lemma foo {a1 a2} : a1 = a2 -> a1 + a1 = a2 + a2.
Fail progress case.

(* Either one works, and gives a goal that can be dispatches by reflexivity. *)

Blaisorblade

module foo where
open import Data.Nat
open import Agda.Primitive
open import Level
foo = λ (T : (∀ (X : Set (lsuc lzero)) → X → X)) (X : Set lzero) → T (Lift _ X)

Blaisorblade

data _≡_ {i} {A : Set i} (x : A) : A -> Set i where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

data Unit : Set where
  unit : Unit

refl_unit : unit ≡ unit
refl_unit = refl

Blaisorblade

From iris.algebra Require Import ofe.

Import EqNotations.
Unset Program Cases.

(* Subsumed by https://gitlab.mpi-sws.org/iris/stdpp/commit/4978faed45d1a1d84f79d3ec0456dd55d831b684 *)
Definition proj1_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : P :=
  let '(ex_intro _ x _) := p in x.
Definition proj2_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : Q (proj1_ex p) :=
  let '(ex_intro _ x H) := p in H.

Blaisorblade

From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.

Section foo.
  Context `{Σ : gFunctors}.

  Goal True ⊢ True : iProp Σ.
  Proof.
    iIntros.
    (* Solves the goal, but needs the parens. *)

Blaisorblade

object Init {
  class Circular[A](val value: A, getter: => Circular[A]) {
    lazy val get: Circular[A] = getter
  }

  def create[A](as: Traversable[A]): Circular[A] = {
    def go[A](as: Traversable[A], initTail: => Circular[A]): Circular[A] = {
      if (as.nonEmpty)
        new Circular(as.head, go(as.tail, initTail))
      else

Blaisorblade

object Test {
  abstract class ExprBase { s =>
    type A
  }

  abstract class Lit extends ExprBase { s =>
    type A = Int
    val n: A
  }

Blaisorblade

Require Import Coq.ssr.ssreflect.
Require Import ProofIrrelevance.

Definition bad_sigma_irrelevance :=
  (* Beware this P is in Type, not Prop; that's why this is inconsistent. *)
  (* forall (U:Type) (P:U->Type) (x y:U) (p:P x) (q:P y), *)
  (* equivalently: *)
  forall (U:Type) P (x y: U) (p:P x) (q:P y),
    x = y -> existT P x p = existT P y q.

Blaisorblade

From iris.base_logic.lib Require Import iprop.

Section test.
  Context `(Σ : gFunctors).
  Import iProp_solution.
  Import cofe_solver.
  (* There is some duplication from https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/iprop.v#L135-136. *)
  (*  That's needed here because iProp_result is hidden, so we re-define it. *)
  Definition iProp_result :
      solution (uPredCF (iResF Σ)) := solver.result (uPredCF (iResF Σ)).