D.Dot.syn.core_stamping_defs
Define "stamping" in a purely syntactic
way, without involving Iris.
From D.Dot Require Import syn traversals typing_aux_defs.
Export typing_aux_defs.
Set Implicit Arguments.
Import Trav1.
Implicit Types
(T : ty) (v : vl) (e : tm) (p : path) (d : dm) (ds : dms) (vs : vls)
(Γ : ctx) (n : nat).
Export typing_aux_defs.
Set Implicit Arguments.
Import Trav1.
Implicit Types
(T : ty) (v : vl) (e : tm) (p : path) (d : dm) (ds : dms) (vs : vls)
(Γ : ctx) (n : nat).
Proposition is_unstamped_path n OnlyVars p implies that p is an
unstamped path in the strict sense defined in the paper; in particular, it's
also a stamped path.
Instead, is_unstamped_path n AllowNonVars p implies that p can be a
generic stable term.
Inductive AllowNonVars := OnlyVars | AlsoNonVars.
Definition is_unstamped_trav : Traversal (nat × AllowNonVars) :=
{|
upS := λ '(n, b), (n.+1, b);
underPathElimS := λ '(n, _), (n, OnlyVars);
varP := λ '(n, b) i, i < n;
dtysynP := λ _ T, True;
dtysemP := λ _ vs s T' ts', False;
pathRootP := λ '(n, b) v, b = AlsoNonVars ∨
(∃ x, v = vvar x) ∨ (∃ l, v = vlit l);
|}.
Notation is_unstamped_tm n b := (forall_traversal_tm is_unstamped_trav (n, b)).
Notation is_unstamped_vl n b := (forall_traversal_vl is_unstamped_trav (n, b)).
Notation is_unstamped_dm n b := (forall_traversal_dm is_unstamped_trav (n, b)).
Notation is_unstamped_path n b := (forall_traversal_path is_unstamped_trav (n, b)).
Notation is_unstamped_ty n b := (forall_traversal_ty is_unstamped_trav (n, b)).
Notation is_unstamped_kind n b := (forall_traversal_kind is_unstamped_trav (n, b)).
Notation is_unstamped_path' n := (is_unstamped_path n OnlyVars).
Notation is_unstamped_ty' n := (is_unstamped_ty n OnlyVars).
Notation is_unstamped_kind' n := (is_unstamped_kind n OnlyVars).
Ltac with_is_unstamped tac := with_forall_traversal is_unstamped_trav tac.
Ltac inverse_is_unstamped := inverse_forall_traversal is_unstamped_trav.
Lemma is_unstamped_path_root n p :
is_unstamped_path n OnlyVars p →
atomic_path_root p.
Proof. elim p ⇒ /= *; with_is_unstamped inverse; naive_solver. Qed.