Add unscoped syntax

Makefile

@@ -16,12 +16,12 @@ uninstall: $(COQMAKEFILE)
 	$(MAKE) -f $(COQMAKEFILE) uninstall
 
 theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
-	autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig
+	autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig
 
 .PHONY: clean FORCE
 
 clean:
 	test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )
-	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v
 
 FORCE:

syntax.sig

@@ -16,7 +16,6 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
 PUniv : nat -> PTm
-PBot : PTm
 PNat : PTm
 PZero : PTm
 PSuc : PTm -> PTm

theories/Autosubst2/unscoped.v

@@ -0,0 +1,213 @@
+(** * Autosubst Header for Unnamed Syntax
+
+Version: December 11, 2019.
+ *)
+
+(* Adrian:
+ I changed this library a bit to work better with my generated code.
+ 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
+ 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
+Require Import core.
+Require Import Setoid Morphisms Relation_Definitions.
+
+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 shift  := S.
+
+Definition var_zero := 0.
+
+Definition id {X} := @Datatypes.id X.
+
+Definition scons {X: Type} (x : X) (xi : nat -> X) :=
+  fun n => match n with
+        | 0 => x
+        | S n => xi n
+        end.
+
+#[ export ]
+Hint Opaque scons : rewrite.
+
+(** ** Type Class Instances for Notation
+Required to make notation work. *)
+
+(** *** Type classes for renamings. *)
+
+Class Ren1 (X1  : Type) (Y Z : Type) :=
+  ren1 : X1 -> Y -> Z.
+
+Class Ren2 (X1 X2 : Type) (Y Z : Type) :=
+  ren2 : X1 -> X2 -> Y -> Z.
+
+Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) :=
+  ren3 : X1 -> X2 -> X3 -> Y -> Z.
+
+Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) :=
+  ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
+
+Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) :=
+  ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
+
+Module RenNotations.
+  Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s  ⟨ xi1 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4  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 ⟩" := (ren5  xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.
+
+  Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.
+
+  Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.
+End RenNotations.
+
+(** *** Type Classes for Substiution *)
+
+Class Subst1 (X1 : Type) (Y Z: Type) :=
+  subst1 : X1 -> Y -> Z.
+
+Class Subst2 (X1 X2 : Type) (Y Z: Type) :=
+  subst2 : X1 -> X2 -> Y  -> Z.
+
+Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) :=
+  subst3 : X1 -> X2 -> X3 ->  Y  -> Z.
+
+Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) :=
+  subst4 : X1 -> X2 -> X3 -> X4 -> Y  -> Z.
+
+Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) :=
+  subst5 : X1 -> X2 -> X3 -> X4 -> X5  -> Y  -> Z.
+
+Module SubstNotations.
+  Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.
+
+  Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/'  tau ]") : subst_scope.
+End SubstNotations.
+
+(** *** Type Class for Variables *)
+
+Class Var X Y :=
+  ids : X -> Y.
+
+#[export] Instance idsRen : Var nat nat := id.
+
+(** ** Proofs for the substitution primitives. *)
+
+Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.
+
+Module CombineNotations.
+  Notation "f >> g" := (funcomp g f) (at level 50) : fscope.
+
+  Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope.
+
+  #[ global ]
+  Open Scope fscope.
+  #[ global ]
+  Open Scope subst_scope.
+End CombineNotations.
+
+Import CombineNotations.
+
+
+(** A generic lifting of a renaming. *)
+Definition up_ren (xi : nat -> nat) :=
+  0 .: (xi >> S).
+
+(** A generic proof that lifting of renamings composes. *)
+Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) :
+  forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
+Proof.
+  intros [|x].
+  - reflexivity.
+  - unfold up_ren. cbn. unfold funcomp. f_equal. apply E.
+Qed.
+
+(** Eta laws. *)
+Lemma scons_eta' {T} (f : nat -> T) :
+  pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_eta_id' :
+  pointwise_relation _ eq (var_zero .: shift) id.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) :
+  pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
+Proof. intros x. destruct x; reflexivity. Qed.
+
+(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
+#[export] Instance scons_morphism {X: Type} :
+  Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X).
+Proof.
+  intros ? t -> sigma tau H.
+  intros [|x].
+  cbn. reflexivity.
+  apply H.
+Qed.
+
+#[export] Instance scons_morphism2 {X: Type} :
+  Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X).
+Proof.
+  intros ? t -> sigma tau H ? x ->.
+  destruct x as [|x].
+  cbn. reflexivity.
+  apply H.
+Qed.
+
+(** ** Generic lifting of an allfv predicate *)
+Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p.
+
+(** ** Notations for unscoped syntax *)
+Module UnscopedNotations.
+  Include RenNotations.
+  Include SubstNotations.
+  Include CombineNotations.
+  
+  (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
+
+  Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
+
+  Notation "↑" := (shift) : subst_scope.
+
+  #[global]
+  Open Scope fscope.
+  #[global]
+  Open Scope subst_scope.
+End UnscopedNotations.
+
+(** ** Tactics for unscoped syntax *)
+
+(** 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
+                                           | [|- forall (i : nat), _] => intros []; t
+                                           end).
+
+
+(** Generic fsimpl tactic: simplifies the above primitives in a goal. *)
+Ltac fsimpl :=
+  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))
+         | [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v
+         | [|- 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 >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
+         | [|- context[var_zero]] =>  change var_zero with 0
+         | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f)
+         | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta'
+         | [|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
+         | [|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
+         (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *)
+         | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
+         | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce
+                        end.

theories/common.v

@@ -1,41 +1,52 @@
-Require Import Autosubst2.fintype Autosubst2.syntax Autosubst2.core ssreflect.
+Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect.
 From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
 From Hammer Require Import Tactics.
 
-Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
+Inductive lookup : nat -> list PTm -> PTm -> Prop :=
-  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
+| here A Γ : lookup 0 (cons A Γ) (ren_PTm shift A)
+| there i Γ A B :
+  lookup i Γ A ->
+  lookup (S i) (cons B Γ) (ren_PTm shift A).
 
-Lemma up_injective n m (ξ : fin n -> fin m) :
+Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) :=
-  (forall i j, ξ i = ξ j -> i = j) ->
+  forall i A, lookup i Δ A -> lookup (ξ i) Γ (ren_PTm ξ A).
-  forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
+
+Definition ren_inj (ξ : nat -> nat) := forall i j, ξ i = ξ j -> i = j.
+
+Lemma up_injective (ξ : nat -> nat) :
+  ren_inj ξ ->
+  ren_inj (upRen_PTm_PTm ξ).
 Proof.
-  sblast inv:option.
+  move => h i j.
+  case : i => //=; case : j => //=.
+  move => i j. rewrite /funcomp. hauto lq:on rew:off unfold:ren_inj.
 Qed.
 
 Local Ltac2 rec solve_anti_ren () :=
   let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
   intro $x;
   lazy_match! Constr.type (Control.hyp x) with
-  | fin _ -> _ _ => (ltac1:(case;hauto lq:on rew:off use:up_injective))
+  | nat -> nat => (ltac1:(case => *//=; qauto l:on use:up_injective unfold:ren_inj))
   | _ => solve_anti_ren ()
   end.
 
 Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 
-Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
+Lemma ren_injective (a b : PTm) (ξ : nat -> nat) :
-  (forall i j, ξ i = ξ j -> i = j) ->
+  ren_inj ξ ->
   ren_PTm ξ a = ren_PTm ξ b ->
   a = b.
 Proof.
-  move : m ξ b. elim : n / a => //; try solve_anti_ren.
+  move : ξ b. elim : a => //; try solve_anti_ren.
+  move => p ihp ξ []//=. hauto lq:on inv:PTm, nat ctrs:- use:up_injective.
 Qed.
 
 Inductive HF : Set :=
 | H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot.
 
-Definition ishf {n} (a : PTm n) :=
+Definition ishf (a : PTm) :=
   match a with
   | PPair _ _ => true
   | PAbs _ => true
@@ -47,7 +58,7 @@ Definition ishf {n} (a : PTm n) :=
   | _ => false
   end.
 
-Definition toHF {n} (a : PTm n) :=
+Definition toHF (a : PTm) :=
   match a with
   | PPair _ _ => H_Pair
   | PAbs _ => H_Abs
@@ -59,54 +70,53 @@ Definition toHF {n} (a : PTm n) :=
   | _ => H_Bot
   end.
 
-Fixpoint ishne {n} (a : PTm n) :=
+Fixpoint ishne (a : PTm) :=
   match a with
   | VarPTm _ => true
   | PApp a _ => ishne a
   | PProj _ a => ishne a
-  | PBot => true
   | PInd _ n _ _ => ishne n
   | _ => false
   end.
 
-Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
+Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false.
 
-Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
+Definition isuniv (a : PTm) := if a is PUniv _ then true else false.
 
-Definition ispair {n} (a : PTm n) :=
+Definition ispair (a : PTm) :=
   match a with
   | PPair _ _ => true
   | _ => false
   end.
 
-Definition isnat {n} (a : PTm n) := if a is PNat then true else false.
+Definition isnat (a : PTm) := if a is PNat then true else false.
 
-Definition iszero {n} (a : PTm n) := if a is PZero then true else false.
+Definition iszero (a : PTm) := if a is PZero then true else false.
 
-Definition issuc {n} (a : PTm n) := if a is PSuc _ then true else false.
+Definition issuc (a : PTm) := if a is PSuc _ then true else false.
 
-Definition isabs {n} (a : PTm n) :=
+Definition isabs (a : PTm) :=
   match a with
   | PAbs _ => true
   | _ => false
   end.
 
-Definition ishf_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition ishf_ren (a : PTm)  (ξ : nat -> nat) :
   ishf (ren_PTm ξ a) = ishf a.
 Proof. case : a => //=. Qed.
 
-Definition isabs_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition isabs_ren (a : PTm)  (ξ : nat -> nat) :
   isabs (ren_PTm ξ a) = isabs a.
 Proof. case : a => //=. Qed.
 
-Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition ispair_ren (a : PTm)  (ξ : nat -> nat) :
   ispair (ren_PTm ξ a) = ispair a.
 Proof. case : a => //=. Qed.
 
-Definition ishne_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition ishne_ren (a : PTm)  (ξ : nat -> nat) :
   ishne (ren_PTm ξ a) = ishne a.
-Proof. move : m ξ. elim : n / a => //=. Qed.
+Proof. move : ξ. elim : a => //=. Qed.
 
-Lemma renaming_shift n m Γ (ρ : fin n -> PTm m) A :
+Lemma renaming_shift Γ (ρ : nat -> PTm) A :
-  renaming_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) Γ shift.
+  renaming_ok (cons A Γ) Γ shift.
-Proof. sfirstorder. Qed.
+Proof. rewrite /renaming_ok. hauto lq:on ctrs:lookup. Qed.