Refactor context file to use sigma library

takanuva · Oct 2, 2024 · 1b202e3 · 1b202e3
1 parent 3e6933e
commit 1b202e3
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 0 deletions.
diff --git a/theories/Context.v b/theories/Context.v
@@ -8,6 +8,7 @@ Require Export Setoid.
 Require Export Relations.
 Require Import Equality.
 Require Import Local.Prelude.
+Require Import Local.Substitution.
 Require Import Local.Syntax.
 Require Import Local.Metatheory.
 

diff --git a/theories/Metatheory.v b/theories/Metatheory.v
@@ -1251,3 +1251,24 @@ Proof with modulo_arith.
       rewrite Nat.add_comm.
       assumption.
 Qed.
+
+Lemma apply_parameters_unfold:
+  forall y ys k e,
+  apply_parameters (y :: ys) k e = subst y k (apply_parameters ys (1 + k) e).
+Proof.
+  intros.
+  unfold apply_parameters.
+  now sigma.
+Qed.
+
+Lemma right_cycle_characterization:
+  forall i k e,
+  right_cycle i k e =
+    apply_parameters (high_sequence i ++ [bound 0]) k (lift (S i) (S i + k) e).
+Proof.
+  intros.
+  unfold right_cycle.
+  unfold apply_parameters.
+  assert (length (high_sequence i) = i) by apply sequence_length.
+  now sigma.
+Qed.