Require Export Forms. Set Implicit Arguments. (* definition of terms S:= F|(S,S)*) Inductive context : Set := | form : Form -> context | bin : context -> context -> context. Notation "Gamma 'oo' Gamma'" := (bin Gamma Gamma') (at level 50, left associativity):lbk_scope. Notation "^ A" := (form A) (at level 40). (* how to deal with Gamma[Delta] meta notation *) (* prolog-like way *) (* replace Delta Delta' Gamma Gamma' means : Gamma = Gamma0[Delta] and Gamma'=Gamma0[Delta'] replacement at one location (one hole in Gamma0) *) Inductive replace (Delta Delta':context): context -> context -> Set := | replaceRoot : replace Delta Delta' Delta Delta' | replaceLeft : forall (Gamma1 Gamma2 Gamma3:context), replace Delta Delta' Gamma1 Gamma2 -> replace Delta Delta' (bin Gamma1 Gamma3) (bin Gamma2 Gamma3) | replaceRight : forall (Gamma1 Gamma2 Gamma3:context), replace Delta Delta' Gamma1 Gamma2 -> replace Delta Delta' (bin Gamma3 Gamma1) (bin Gamma3 Gamma2). (* Using Huet's zippers *) Inductive zcontext : Set := (* context with 1 hole *) | zroot : zcontext | zleft : zcontext -> context -> zcontext | zright : context-> zcontext -> zcontext. Fixpoint zfill (z:zcontext)(Gamma : context) {struct z} : context := match z with zroot => Gamma | zleft z1 Gamma2 => zfill z1 (Gamma oo Gamma2) | zright Gamma1 z2 => zfill z2 (Gamma1 oo Gamma) end. Fixpoint zgraft (z z': zcontext){struct z} : zcontext := match z with | zroot => z' | zleft zc1 c2 => zleft (zgraft zc1 z') c2 | zright c1 zc2 => zright c1 (zgraft zc2 z') end. Lemma zgraft_def : forall z z' c, zfill (zgraft z z') c = zfill z' (zfill z c). induction z. simpl. auto. intros; simpl; auto. intros; simpl; auto. Qed. Definition zfill_to_replace_0 : forall (Delta1 Delta2: context)(ZGamma : zcontext) (Gamma1 Gamma2:context), replace Delta1 Delta2 Gamma1 Gamma2 -> replace Delta1 Delta2 (zfill ZGamma Gamma1) (zfill ZGamma Gamma2). induction ZGamma. simpl;auto. simpl; intros. apply IHZGamma. constructor 2. auto. simpl; intros. apply IHZGamma. constructor 3. auto. Defined. Definition zfill_to_replace : forall (ZGamma : zcontext)(Delta1 Delta2: context), replace Delta1 Delta2 (zfill ZGamma Delta1) (zfill ZGamma Delta2). intros; apply zfill_to_replace_0. constructor 1. Defined. Definition replace_to_zfill: forall (Delta1 Delta2 Gamma1 Gamma2: context), replace Delta1 Delta2 Gamma1 Gamma2 -> {ZGamma : zcontext | zfill ZGamma Delta1 = Gamma1 /\ zfill ZGamma Delta2 = Gamma2}. induction 1. exists zroot. simpl; split; auto. case IHreplace; intros Z1 [e1 e2]. exists (zgraft Z1 (zleft zroot Gamma3)). rewrite zgraft_def. rewrite zgraft_def. simpl. rewrite e1;rewrite e2; auto. case IHreplace; intros Z1 [e1 e2]. exists (zgraft Z1 (zright Gamma3 zroot)). rewrite zgraft_def. rewrite zgraft_def. simpl. simpl. rewrite e1;rewrite e2; auto. Defined. Fixpoint context_to_form (Gamma : context){ struct Gamma} : Form := match Gamma with | form f => f | Gamma1 oo Gamma2 => (context_to_form Gamma1) o (context_to_form Gamma2) end.