Library Context

This library defines the type context of infinite one-hole contexts whose holes are at a finite depth.

Require Import Prelims.
Require Export Term.
Require Export TermEquality.
Require Import Equality.

Set Implicit Arguments.

Section Context.

Contexts are defined inductively over a signature F and a set of variables X.

Variable F : signature.
Variable X : variables.

Notation term := (term F X).
Notation terms := (vector term).

One-hole contexts where a hole can occur at any finite depth.

Inductive context : Type :=
  | Hole : context
  | CFun : forall (f : F) (i j : nat),
           i + S j = arity f -> terms i -> context -> terms j -> context.

Implicit Arguments CFun [i j].

Depth of a hole.

Fixpoint hole_depth c : nat :=
  match c with
  | Hole => 0
  | CFun _ _ _ _ _ c' _ => 1 + hole_depth c'
  end.

Position of a hole.

Fixpoint hole_position c : position :=
  match c with
  | Hole => nil
  | CFun _ i _ _ _ c' _ => i :: (hole_position c')
  end.

Depth of a hole is depth of its position.

Lemma hole_position_depth :
forall c,
hole_depth c = position_depth (hole_position c).
Proof.
induction c; simpl; try (rewrite IHc); reflexivity.
Qed.

Fill a hole in a context with a term.

Fixpoint fill (c : context) (t : term) : term :=
  match c with
  | Hole => t
  | CFun f i j H v1 c' v2 => Fun f (vcast (vappend v1 (vcons (fill c' t) v2)) H)
  end.

Filling a context gives terms equal up to the hole depth.

Lemma fill_eq_up_to :
forall (c : context) t u n,
n <= hole_depth c -> term_eq_up_to n (fill c t) (fill c u).
Proof.
intros c t u n.
revert c.
induction n as [| n IH]; simpl.
constructor.
destruct c; simpl; intro H.
inversion H.
constructor.
revert v e.
generalize (arity f).
induction i as [| i IHi]; simpl; intro a.
intros _ e k.
destruct k; repeat (rewrite vcast_vcons).
apply IH.
auto with arith.
apply term_eq_refl.
intros v e k.
destruct k; repeat (rewrite vcast_vcons).
apply term_eq_refl.
apply IHi.
Qed.

Filling a context with bisimilar terms yields bisimilar terms.

Lemma fill_term_bis :
  forall (c : context) t u,
    t [~] u ->
    fill c t [~] fill c u.
Proof.
intros c t u H.
induction c as [| f i j H1 v1 c IH v2]; simpl.
assumption.
constructor.
intro k.
destruct H1.
simpl.
induction i as [| i IHi].
simpl in k.
simpl.
dependent destruction k.
simpl.
assumption.
apply term_bis_refl.
dependent destruction k.
apply term_bis_refl.
specialize IHi with (vtail v1) k.
simpl.
assumption.
Qed.

Require Import Arith.

Lemma lt_plus_minus_r : forall n m, n < m -> n + S (m - S n) = m.
intros.
rewrite <- plus_Snm_nSm.
apply le_plus_minus_r.
assumption.
Qed.

Require Import Lt.
Require Import Bool_nat.

Create a context from a term by making a hole.

Fixpoint dig (t : term) (p : position) {struct p} : option context :=
  match p with
  | nil => Some Hole
  | n :: p => match t with
              | Var _ => None
              | Fun f args => match lt_ge_dec n (arity f) with
                              | left h => match dig (vnth h args) p with
                                           | None => None
                                           | Some c => Some (CFun f (lt_plus_minus_r h)
                                                                  (vtake (lt_le_weak n (arity f) h) args)
                                                                  c
                                                                  (vdrop h args))
                                           end
                              | right _ => None
                              end
              end
  end.

Digging a hole and filling it with the same gets you nothing new.

Lemma dig_fill :
  forall t p,
    match dig t p, subterm t p with
    | Some c, Some s => fill c s [=] t
    | _, _ => True
    end.
Proof.
intros t p.
induction p as [| n p IH]; simpl.
apply term_eq_refl.

By the way, CoLoR states it like this:

Lemma subterm_elim : forall p t s, subterm t p = Some s ->
  {c | dig s p = Some c /\ s [=] fill c s}.

End Context.

Implicit Arguments Hole [F X].