Autosubst Header for Unnamed Syntax

Version: December 11, 2019.

Require Export axioms.

Definition ap {X Y} (f : X Y) {x y : X} (p : x = y) : f x = f y :=
match p with eq_refl eq_refl end.

Definition apc {X Y} {f g : X Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
match q with eq_refl match p with eq_refl eq_refl end end.

Primitives of the Sigma Calculus.

Definition None := 0.
Definition Some := S.

Notation fin := .
Definition shift := S.

Definition var_zero := 0.

Definition id {X} (x: X) := x.

Definition scons {X: Type} (x : X) ( : X) :=
   n match n with
          |0 x
          |S n n
          end.

Notation "s .: sigma" := (scons s ) (at level 70).

Definition funcomp {X Y Z} (g : Y Z) (f : X Y) :=
   x g (f x).

Type Class Instances for Notation

Required to make notation work.

Type classes for renamings.

Class Ren1 ( : Type) (Y Z : Type) :=
  ren1 : Y Z.

Class Ren2 ( : Type) (Y Z : Type) :=
  ren2 : Y Z.

Class Ren3 ( : Type) (Y Z : Type) :=
  ren3 : Y Z.

Class Ren4 ( : Type) (Y Z : Type) :=
  ren4 : Y Z.

Class Ren5 ( : Type) (Y Z : Type) :=
  ren5 : Y Z.

Notation "s ⟨ xi1 ⟩" := ( s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope.

Notation "s ⟨ xi1 ; xi2 ⟩" := ( s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope.

Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := ( s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.

Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := ( s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope.

Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := ( s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.

Notation "⟨ xi ⟩" := ( ) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.

Notation "⟨ xi1 ; xi2 ⟩" := ( ) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.

Type Classes for Substiution

Class Subst1 ( : Type) (Y Z: Type) :=
  subst1 : Y Z.

Class Subst2 ( : Type) (Y Z: Type) :=
  subst2 : Y Z.

Class Subst3 ( : Type) (Y Z: Type) :=
  subst3 : Y Z.

Class Subst4 ( : Type) (Y Z: Type) :=
  subst4 : Y Z.

Class Subst5 ( : Type) (Y Z: Type) :=
  subst5 : Y Z.

Notation "s [ sigma ]" := ( s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.

Notation "s [ sigma ; tau ]" := ( s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope.

Type Class for Variables

Class Var X Y :=
ids : X Y.

Proofs for the substitution primitives.

Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.

Notation "f >> g" := (funcomp g f) (*fun x => g (f x)*) (at level 50) : subst_scope.
Open Scope subst_scope.

A generic lifting of a renaming.

Definition up_ren ( : ) :=
0 .: ( >> S ).

A generic proof that lifting of renamings composes.

Lemma up_ren_ren (: ) ( : ) (: ) (E: x, ( >> ) x = x) :
   x, (up_ren >> up_ren ) x = up_ren x.
Proof.
  intros [|x].
  - reflexivity.
  - unfold up_ren. simpl. unfold funcomp. rewrite E. reflexivity.
Qed.

Eta laws.

Lemma scons_eta_id {n : } : var_zero .: shift = id :> ( ).
Proof. fext. intros [|x]; reflexivity. Qed.

Lemma scons_eta {T} (f : T) :
  f var_zero .: shift >> f = f.
Proof. fext. intros [|x]; reflexivity. Qed.

Lemma scons_comp (T: Type) U (s: T) (: T) (: T U ) :
  (s .: ) >> = scons ( s) ( >> ) .
Proof.
  fext. intros [|x]; reflexivity.
Qed.

Notations for unscoped syntax

Generic fsimpl tactic: simplifies the above primitives in a goal.

Ltac fsimpl :=
  unfold up_ren; repeat match goal with
         | [|- context[id >> ?f]] change (id >> f) with f (* AsimplCompIdL *)
         | [|- context[?f >> id]] change (f >> id) with f (* AsimplCompIdR *)
         | [|- context [id ?s]] change (id s) with s
         | [|- context[(?f >> ?g) >> ?h]]
           change ((?f >> ?g) >> ?h) with (f >> (g >> h)) (* AsimplComp *)
         | [|- context[(?s.:?) var_zero]] change ((s.:)var_zero) with s
         | [|- context[(?f >> ?g) >> ?h]]
           change ((f >> g) >> h) with (f >> (g >> h))
        | [|- context[?f >> (?x .: ?g)]]
           change (f >> (x .: g)) with g
         | [|- context[var_zero]] change var_zero with 0
         | [|- context[? .: shift >> ?f]]
           change with (f 0); rewrite (@scons_eta _ _ f)
         | [|- context[(?v .: ?g) 0]]
           change ((v .: g) 0) with v
         | [|- context[(?v .: ?g) (S ?n)]]
           change ((v .: g) (S n)) with (g n)
         | [|- context[?f 0 .: ?g]]
           change g with (shift >> f); rewrite scons_eta
         | _ first [progress (rewrite ?scons_comp) | progress (rewrite ?scons_eta_id)]
end.

Generic fsimpl tactic: simplifies the above primitives in the context

Simplification in both the goal and the context

Tactic Notation "fsimpl" "in" "*" :=
fsimpl; fsimplc.

Notation "s , sigma" := (scons s ) (at level 60, format "s , sigma", right associativity) : subst_scope.

Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
Instance idsRen : Var := id.

Notation "↑" := (shift).

Tactics for unscoped syntax

Unfold of the instances in goal and context.

Ltac auto_unfold := unfold , , , , ids; unfold Subst1, Ren1, Subst2, Ren2, Var.

Ltac unfold_funcomp := match goal with
| |- context[(?f >> ?g) ?s] change ((f >> g) s) with (g (f s))
end.

Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms.

Tactic Notation "auto_case" tactic(t) := (match goal with
| [|- (i : ), _] intros []; t
end).