Module contexts

This development makes use of contexts to define the semantics of various constructs. This file collects some general purpose definitions, theorems, and tactics.
Require Export list.

Contexts with one hole

The most commonly used kind of context is the one with exactly one hole. A context equipped with a value for its hole is known as a zipper. We define an operational type class for substitution. The function subst E x is supposed to substitute the value x in the hole of the context E.
Class Subst A B C := subst: ABC.
Instance: Params (@subst) 4.
Arguments subst {_ _ _ _} !_ _ / : simpl nomatch.

We generally define contexts as lists of singular contexts. For example for binary trees Inductive tree := leaf | branch : treetreetree, we would first define Inductive tree_ctx := branchL : treetree_ctx | branchR : treetree_ctx, and then the actual context is defined as list tree_ctx. A pair tree * list tree_ctx is a zipper, where the second projection is a tree turned inside-out representing a path from the top.
We define subsitution for contexts as singular contexts in a generic way.
Instance list_subst `{Subst A B B} : Subst (list A) B B :=
  fix go (l : list A) (b : B) : B := let _ : Subst _ _ _ := @go in
  match l with [] => b | a :: l => subst l (subst a b) end.
Lemma subst_nil `{Subst A B B} b : subst [] b = b.
Proof. done. Qed.
Lemma subst_app `{Subst A B B} (l1 l2 : list A) b :
  subst (l1 ++ l2) b = subst l2 (subst l1 b).
Proof. revert b. induction l1; simpl; auto. Qed.
Lemma subst_snoc `{Subst A B B} (l1 : list A) a b :
  subst (l1 ++ [a]) b = subst a (subst l1 b).
Proof. exact (subst_app l1 [a] b). Qed.

Instance list_subst_injective `{Subst A B B} :
  (∀ a, Injective (=) (=) (subst a)) →
  ∀ l : list A, Injective (=) (=) (subst l).
Proof.
  intros ? l. red. induction l as [|x l IH]; simpl; intros; auto.
  eapply (injective (subst _)), IH; eassumption.
Qed.


Contexts with multiple holes

Less commonly used kinds of contexts are those with multiple holes. These can be represented as dependent types indexed by the number of holes. We define a class DepSubst for substitution. The function depsubst E xs is supposed to substitute the values of the vector xs in the holes of E.
Class DepSubst {I} (A : IType) (B : IType) C :=
  depsubst : ∀ {i}, A iB iC.
Instance: Params (@depsubst) 6.
Arguments depsubst {_ _ _ _ _ _} !_ _ / : simpl nomatch.

Tactics

The tactic simplify_subst_equality H simplifies an assumption H that is an equality involving subst. It repeatedly tries to use injectivity of subst, or to perform case analysis on the context. Such case analyses are only performed for contexts for which an instance of DestructSubst is declared.
Class DestructSubst `(Subst A B C) := {}.

Tactic Notation "simplify_subst_equality" hyp(H) :=
  match type of H with
  | subst ?a _ = subst ?a _ => apply (injective a) in H
  | @subst _ _ _ ?sub ?a _ = _ =>
    is_var a; let ssub := constr:(_ : DestructSubst sub) in
    destruct a; first [discriminate H | injection' H]
  | _ = @subst _ _ _ ?sub ?a _ =>
    is_var a; let ssub := constr:(_ : DestructSubst sub) in
    destruct a; first [discriminate H | injection' H]
  end;
  list_simplifier.
Tactic Notation "simplify_subst_equality" :=
  repeat_on_hyps (fun H => simplify_subst_equality H);
  list_simplifier.

The tactic simplify_list_subst_equality behaves like the previous tactic, but then for the case of lists as contexts.
Tactic Notation "simplify_list_subst_equality" hyp(H) :=
  match type of H with
  | subst ?l _ = subst ?l _ => apply (list_subst_injective _ l) in H
  | @subst _ _ _ list_subst ?l _ = _ =>
     destruct l as [|?? _] using rev_ind;
       [ rewrite subst_nil in H; simplify_equality
       | rewrite subst_snoc in H; simplify_subst_equality H]
  | _ = @subst _ _ _ list_subst ?l _ =>
     destruct l as [|?? _] using rev_ind;
       [ rewrite subst_nil in H; simplify_equality
       | rewrite subst_snoc in H; simplify_subst_equality H]
  | _ => simplify_subst_equality H
  end.
Tactic Notation "simplify_list_subst_equality" :=
  repeat_on_hyps (fun H => simplify_list_subst_equality H);
  list_simplifier.