Trans closure

polymorphism/README.md

@@ -7,16 +7,19 @@ The $λ^\diamond$-calculus [1], a refined reachability model that scales to para
 * [`Base`](lambda_diamond_base) -- Base system introducing the new reachability model, lacking type polymorphism.
 * [`Fsub`](f_sub_diamond) -- Bounded type-and-reachability polymorphism.
 * [`Fsub-Trans`](f_sub_trans) -- Bounded type-and-reachability polymorphism with explicit transitive closure.
+* [`Fsub-Cycles-Nat`](f_sub_cycles_nat) -- Bounded type-and-reachability polymorphism with cyclic references and natural numbers.
 
 ```mermaid
 graph TD
     subgraph poly[Polymorphism]
       Base
       Fsub
 	  Fsub-Trans
+	  Fsub-Cycles-Nat
     end
     Base-->Fsub
 	Base-->Fsub-Trans
+	Trans-->Fsub-Cycles-Nat
 ```
 
 [`Fsub-Trans`](f_sub_trans) should be considered as the reference mechanization of the $F_{<:}^\diamond$-calculus from POPL '24.

polymorphism/f_sub_cycles_nat/_CoqProject

@@ -0,0 +1,13 @@
+-R . Top
+boolean.v
+env.v
+examples.v
+f_sub_cycles_nat.v
+lang.v
+nats.v
+qenv.v
+qualifiers_base.v
+qualifiers_slow.v
+qualifiers.v
+tactics.v
+vars.v

polymorphism/f_sub_cycles_nat/boolean.v

@@ -0,0 +1,82 @@
+Require Import tactics.
+Require Import Coq.Bool.Bool.
+Require Import Coq.Program.Equality.
+Require Import Coq.Logic.PropExtensionality.
+
+#[global] Hint Resolve orb_prop_intro orb_prop_elim andb_prop_intro andb_prop_elim negb_prop_intro negb_prop_elim: core.
+
+Lemma and_prop_l : forall b1 b2, Is_true (b1 && b2) -> Is_true b1.
+intros. apply andb_prop_elim in H. intuition.
+Qed.
+
+Lemma and_prop_r : forall b1 b2, Is_true (b1 && b2) -> Is_true b2.
+intros. apply andb_prop_elim in H. intuition.
+Qed.
+
+Lemma negb_prop : forall b1, Is_true (negb b1) -> Is_true b1 -> False.
+intros. apply negb_prop_elim in H. intuition.
+Qed.
+
+Lemma implb_prop_intro : forall a b,
+  (Is_true a -> Is_true b) -> Is_true (implb a b).
+intros. destruct a; intuition.
+Qed.
+
+Lemma implb_prop_elim : forall a b,
+  Is_true (implb a b) -> Is_true a -> Is_true b.
+intros. destruct a; intuition.
+Qed.
+
+Lemma is_true_lift : forall a b, Is_true a = Is_true b -> a = b.
+intros. destruct a; destruct b; simpl in *; auto.
+  - exfalso. rewrite <- H. apply I.
+  - exfalso. rewrite H. apply I.
+Qed.
+Lemma is_true_lift' : forall a b, a = b -> Is_true a = Is_true b.
+intros. subst. auto.
+Qed.
+
+Lemma Is_true_eq_false : forall a,
+  ~Is_true a -> a = false.
+intros. unfold Is_true,not in H. destruct a; auto. exfalso. auto. 
+Qed.
+
+Lemma Is_true_eq_false_left : forall a,
+  a = false -> ~Is_true a.
+intros. unfold Is_true. rewrite H. auto.
+Qed.
+
+Lemma Is_true_eq_false_right : forall a,
+  false = a -> ~Is_true a.
+intros. unfold Is_true. rewrite <- H. auto.
+Qed.
+
+#[global] Hint Resolve Is_true_eq_true Is_true_eq_left Is_true_eq_right Is_true_eq_false Is_true_eq_false_left Is_true_eq_false_right and_prop_l and_prop_r negb_prop implb_prop_intro implb_prop_elim : core.
+
+Lemma is_true_reflect : forall {b}, reflect (Is_true b) b.
+intros. destruct b; constructor; auto.
+Qed.
+
+Lemma is_true_lift_or : forall a b ,
+  Is_true (a || b) = (Is_true a \/ Is_true b).
+intros. apply propositional_extensionality. intuition.
+Qed.
+
+Lemma is_true_lift_and : forall a b ,
+  Is_true (a && b) = (Is_true a /\ Is_true b).
+intros. apply propositional_extensionality. intuition eauto.
+Qed.
+
+Lemma is_true_lift_not : forall a ,
+  Is_true (negb a) = ~Is_true a.
+intros. apply propositional_extensionality. intuition eauto.
+Qed.
+
+Lemma is_true_lift_implb : forall a b,
+  Is_true (implb a b) = (Is_true a -> Is_true b).
+intros. apply propositional_extensionality. intuition eauto.
+Qed.
+
+#[global] Hint Rewrite is_true_lift_or is_true_lift_and is_true_lift_not is_true_lift_implb : blift_rewrite.
+
+Ltac blift := autorewrite with blift_rewrite in *.

polymorphism/f_sub_cycles_nat/env.v

@@ -0,0 +1,229 @@
+Require Export Arith.EqNat.
+Require Export Arith.Le.
+Require Import Coq.Arith.Arith.
+Require Import Coq.Program.Equality.
+Require Import Coq.Lists.List.
+Require Import Psatz. (* for lia *)
+Require Import Coq.Arith.Compare_dec.
+Import ListNotations.
+
+Require Import tactics.
+
+(* Theory of envs as lists of deBruijn levels *)
+
+(* update entry *)
+Fixpoint update {A} (σ : list A) (l : nat) (v : A) : list A :=
+  match σ with
+  | [] => σ
+  | a :: σ' =>
+      if (Nat.eqb l (length σ')) then (v :: σ') else (a :: (update σ' l v ))
+  end.
+
+Fixpoint insert {A} (σ : list A) (l : nat) (v : A) : list A :=
+  match σ with
+  | [] => σ
+  | a :: σ' =>
+      if (Nat.eqb l (length σ')) then (a :: v :: σ') else (a :: (insert σ' l v ))
+  end.
+
+(* Look up a free variable (deBruijn level) in env   *)
+Fixpoint indexr {X : Type} (n : nat) (l : list X) : option X :=
+  match l with
+    | [] => None
+    | a :: l' =>
+      if (Nat.eqb n (length l')) then Some a else indexr n l'
+  end.
+
+Lemma indexr_head : forall {A} {x : A} {xs}, indexr (length xs) (x :: xs) = Some x.
+  intros. simpl. destruct (Nat.eqb (length xs) (length xs)) eqn:Heq. auto.
+  apply Nat.eqb_neq in Heq. contradiction.
+Qed.
+
+Lemma indexr_length : forall {A B} {xs : list A} {ys : list B}, length xs = length ys -> forall {x}, indexr x xs = None <-> indexr x ys = None.
+Proof.
+  intros A B xs.
+  induction xs; intros; destruct ys; split; simpl in *; intros; eauto; try lia.
+  - inversion H. destruct (PeanoNat.Nat.eqb x (length xs)). discriminate.
+    specialize (IHxs _ H2 x). destruct IHxs. auto.
+  - inversion H. rewrite <- H2 in H0. destruct (PeanoNat.Nat.eqb x (length xs)). discriminate.
+    specialize (IHxs _ H2 x). destruct IHxs. auto.
+Qed.
+
+Lemma indexr_skip : forall {A} {x : A} {xs : list A} {i}, i <> length xs -> indexr i (x :: xs) = indexr i xs.
+Proof.
+  intros.
+  rewrite <- PeanoNat.Nat.eqb_neq in H. auto.
+  simpl. rewrite H. reflexivity.
+Qed.
+
+Lemma indexr_skips : forall {A} {xs' xs : list A} {i}, i < length xs -> indexr i (xs' ++ xs) = indexr i xs.
+  induction xs'; intros; intuition.
+  replace ((a :: xs') ++ xs) with (a :: (xs' ++ xs)).
+  rewrite indexr_skip. eauto. rewrite app_length. lia. auto.
+Qed.
+
+Lemma indexr_var_some :  forall {A} {xs : list A} {i}, (exists x, indexr i xs = Some x) <-> i < length xs.
+Proof.
+  induction xs; intros; split; intros. inversion H. inversion H0.
+  inversion H. inversion H. simpl in H0. destruct (PeanoNat.Nat.eqb i (length xs)) eqn:Heq.
+  apply Nat.eqb_eq in Heq. rewrite Heq. auto. inversion H.
+  simpl in H. rewrite Heq in H. apply IHxs in H. simpl. lia.
+  simpl. destruct (PeanoNat.Nat.eqb i (length xs)) eqn:Heq.
+  exists a. reflexivity. apply Nat.eqb_neq in Heq. simpl in H.
+  apply IHxs. lia.
+Qed.
+
+(* easier to use for assumptions without existential quantifier *)
+Lemma indexr_var_some' :  forall {A} {xs : list A} {i x}, indexr i xs = Some x -> i < length xs.
+Proof.
+  intros. apply indexr_var_some. exists x. auto.
+Qed.
+Lemma indexr_var_same: forall {A}{xs' xs: list A}{i}{v X X' : A}, Nat.eqb i (length xs) = false ->
+  indexr i (xs' ++ X :: xs) =  Some v -> indexr i (xs' ++ X' :: xs) =  Some v.
+Proof. intros ? ? ? ? ? ? ? E H.  induction xs'.
+  - simpl. rewrite E.  simpl in H. rewrite E in H. apply H.
+  - simpl. rewrite app_length. simpl.
+    destruct (Nat.eqb i  ((length xs')  + S (length xs))) eqn: E'.
+      simpl in H. rewrite app_length in H. simpl in H. rewrite E' in H.
+    rewrite H. reflexivity.
+    simpl in H. rewrite app_length in H. simpl in H. rewrite E' in H.
+    rewrite IHxs'. reflexivity. assumption.
+  Qed.
+
+Lemma indexr_var_none :  forall {A} {xs : list A} {i}, indexr i xs = None <-> i >= length xs.
+Proof.
+  induction xs; intros; split; intros.
+  simpl in *. lia. auto.
+  simpl in H.
+  destruct (PeanoNat.Nat.eqb i (length xs)) eqn:Heq.
+  discriminate. apply IHxs in H. apply Nat.eqb_neq in Heq. simpl. lia.
+  assert (Hleq: i >= length xs). {
+    simpl in H. lia.
+  }
+  apply IHxs in Hleq. rewrite <- Hleq.
+  apply indexr_skip. simpl in H. lia.
+Qed.
+
+Lemma indexr_insert_ge : forall {A} {xs xs' : list A} {x} {y}, x >= (length xs') -> indexr x (xs ++ xs') = indexr (S x) (xs ++ y :: xs').
+  induction xs; intros.
+  - repeat rewrite app_nil_l. pose (H' := H).
+    rewrite <- indexr_var_none in H'.
+    rewrite H'. symmetry. apply indexr_var_none. simpl. lia.
+  - replace ((a :: xs) ++ xs') with (a :: (xs ++ xs')); auto.
+    replace ((a :: xs) ++ y :: xs') with (a :: (xs ++ y :: xs')); auto.
+    simpl. replace (length (xs ++ y :: xs')) with (S (length (xs ++ xs'))).
+    destruct (Nat.eqb x (length (xs ++ xs'))) eqn:Heq; auto.
+    repeat rewrite app_length. simpl. lia.
+Qed.
+
+Lemma indexr_insert_lt : forall {A} {xs xs' : list A} {x} {y}, x < (length xs') -> indexr x (xs ++ xs') = indexr x (xs ++ y :: xs').
+  intros.
+  rewrite indexr_skips; auto.
+  erewrite indexr_skips.
+  erewrite indexr_skip. auto.
+  lia. simpl. lia.
+Qed.
+
+Lemma indexr_insert:  forall {A} {xs xs' : list A} {y}, indexr (length xs') (xs ++ y :: xs') = Some y.
+  intros. induction xs.
+  - replace ([] ++ y :: xs') with (y :: xs'); auto. apply indexr_head.
+  - simpl. rewrite IHxs. rewrite app_length. simpl.
+    destruct (PeanoNat.Nat.eqb (length xs') (length xs + S (length xs'))) eqn:Heq; auto.
+    apply Nat.eqb_eq in Heq. lia.
+Qed.
+
+Lemma indexr_extend : forall  {A} (H' H: list A) x (v:A),
+    indexr x H = Some v <-> indexr x (H'++H) = Some v /\ x < length H. 
+Proof.
+    intros. split; intros; intuition; auto.
+    apply indexr_var_some' in H0 as H0'.
+    assert (Nat.eqb x (length H) = false) as E. eapply Nat.eqb_neq; eauto. lia.
+    rewrite indexr_skips; auto.
+    apply indexr_var_some' in H0. auto.
+    rewrite <- H1. rewrite indexr_skips; auto.
+ Qed.
+
+Lemma indexr_extend1: forall {A} (H: list A) x v (vx: A),
+    indexr x H = Some v <-> indexr x (vx::H) = Some v /\ x < length H. 
+Proof. 
+    intros. split; intros. 
+    eapply indexr_extend with (H' := [vx]) in H0. intuition.
+    erewrite indexr_extend with (H' := [vx]); eauto.
+Qed.
+
+Lemma indexr_at_index: forall {A}{xs xs': list A}{y}{i},
+  Nat.eqb i (length(xs')) = true ->
+  indexr i (xs ++ y :: xs') = Some y.
+Proof.
+  intros. apply Nat.eqb_eq in H. subst.
+  induction xs.
+  - simpl. rewrite Nat.eqb_refl. reflexivity.
+  - simpl.
+    rewrite app_length. simpl. rewrite <- plus_n_Sm. rewrite <- plus_Sn_m.
+    replace (length xs' =? S (length xs) + length xs') with false.
+    assumption. symmetry. rewrite Nat.eqb_neq. lia.
+Qed.
+
+Lemma indexr_hit: forall {A}(xs: list A){i}{x y}, indexr i (x :: xs) = Some y  -> i = length(xs) -> x = y.
+  intros. unfold indexr in H.
+  assert (Nat.eqb i (length xs) = true). eapply Nat.eqb_eq. eauto.
+  rewrite H1 in H. inversion H. eauto.
+Qed.
+
+Lemma update_length : forall {A} {σ : list A} {l v}, length σ = length (update σ l v).
+  induction σ; simpl; intuition.
+  destruct (Nat.eqb l (length σ)) eqn:Heq; intuition.
+  simpl. congruence.
+Qed.
+
+Lemma update_indexr_miss : forall {A} {σ : list A} {l v l'}, l <> l' ->  indexr l' (update σ l v) = indexr l' σ.
+  induction σ; simpl; intuition.
+  destruct (Nat.eqb l (length σ)) eqn:Hls; destruct (Nat.eqb l' (length σ)) eqn:Hl's.
+  apply Nat.eqb_eq in Hls. apply Nat.eqb_eq in Hl's. rewrite <- Hl's in Hls. contradiction.
+  simpl. rewrite Hl's. auto.
+  simpl. rewrite <- update_length. rewrite Hl's. auto.
+  simpl. rewrite <- update_length. rewrite Hl's. apply IHσ. auto.
+Qed.
+
+Lemma update_indexr_hit : forall {A} {σ : list A} {l v}, l < length σ -> indexr l (update σ l v) = Some v.
+  induction σ; simpl; intuition.
+  destruct (Nat.eqb l (length σ)) eqn:Hls.
+  apply Nat.eqb_eq in Hls. rewrite Hls. apply indexr_head.
+  simpl. rewrite <- update_length. rewrite Hls. apply Nat.eqb_neq in Hls.
+  apply IHσ. lia.
+Qed.
+
+Lemma update_commute : forall {A} {σ : list A} {i j vi vj}, i <> j -> (update (update σ i vi) j vj) = (update (update σ j vj) i vi).
+  induction σ; simpl; intuition.
+  destruct (Nat.eqb i (length σ)) eqn:Heq.
+  - assert (Heq' : Nat.eqb j (length σ) = false).
+    apply Nat.eqb_eq in Heq. rewrite Nat.eqb_neq. lia.
+    rewrite Heq'. simpl. rewrite Heq'. rewrite <- update_length.
+    rewrite Heq. auto.
+  - destruct (Nat.eqb j (length σ)) eqn:Heq'; simpl.
+    all: repeat rewrite <- update_length.
+    all: rewrite Heq. all: rewrite Heq'. auto.
+    rewrite IHσ; auto.
+Qed.
+
+Lemma update_inv : forall {A} {l : list A} {i v}, i > length l -> update l i v = l.
+Proof.
+  induction l; intros; simpl; auto.
+  bdestruct (i =? length l). simpl in H. lia.
+  bdestruct (i <? length l). simpl in H. lia.
+  assert (length l < i) by lia. f_equal. apply IHl. auto.
+Qed.
+
+Lemma indexr_skips' : forall {A} {xs xs' : list A} {i}, i >= length xs -> indexr i (xs' ++ xs) = indexr (i - length xs) xs'.
+  induction xs; intros; intuition.
+  - rewrite app_nil_r. simpl. rewrite Nat.sub_0_r. auto.
+  - simpl in *. destruct i; try lia.
+    rewrite <- indexr_insert_ge; try lia.
+    rewrite IHxs. simpl. auto. lia.
+Qed.
+
+Fixpoint delete_nth (n : nat) {A} (l : list A) : list A :=
+  match l with
+  | nil       => nil
+  | cons x xs => if (Nat.eqb n (length xs)) then xs else x :: (delete_nth n xs)
+  end.