Compare commits
10 commits
master
...
bove-capre
| Author | SHA1 | Date | |
|---|---|---|---|
| 3efca4160b | |||
| 7b5e9f2562 | |||
| 816c73cb71 | |||
| ca73b5eac6 | |||
| 44ba3e6575 | |||
|
11bfed2d17 | ||
|
|
757f050d92 | ||
|
|
7503dea251 | ||
|
|
6c11f5560d | ||
|
|
875db75955 |
6 changed files with 857 additions and 993 deletions
4
Makefile
4
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/fintype.v theories/Autosubst2/unscoped.v
|
||||
|
||||
FORCE:
|
||||
|
|
|
|||
|
|
@ -1,419 +0,0 @@
|
|||
(** * Autosubst Header for Scoped Syntax
|
||||
Our development utilises well-scoped de Bruijn syntax. This means that the de Bruijn indices are taken from finite types. As a consequence, any kind of substitution or environment used in conjunction with well-scoped syntax takes the form of a mapping from some finite type _I^n_. In particular, _renamings_ are mappings _I^n -> I^m_. Here we develop the theory of how these parts interact.
|
||||
|
||||
Version: December 11, 2019.
|
||||
*)
|
||||
Require Import core.
|
||||
Require Import Setoid Morphisms Relation_Definitions.
|
||||
|
||||
Set Implicit Arguments.
|
||||
Unset Strict Implicit.
|
||||
|
||||
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
|
||||
We implement the finite type with _n_ elements, _I^n_, as the _n_-fold iteration of the Option Type. _I^0_ is implemented as the empty type.
|
||||
*)
|
||||
|
||||
Fixpoint fin (n : nat) : Type :=
|
||||
match n with
|
||||
| 0 => False
|
||||
| S m => option (fin m)
|
||||
end.
|
||||
|
||||
(** Renamings and Injective Renamings
|
||||
_Renamings_ are mappings between finite types.
|
||||
*)
|
||||
Definition ren (m n : nat) : Type := fin m -> fin n.
|
||||
|
||||
Definition id {X} := @Datatypes.id X.
|
||||
|
||||
Definition idren {k: nat} : ren k k := @Datatypes.id (fin k).
|
||||
|
||||
(** We give a special name, to the newest element in a non-empty finite type, as it usually corresponds to a freshly bound variable. *)
|
||||
Definition var_zero {n : nat} : fin (S n) := None.
|
||||
|
||||
Definition null {T} (i : fin 0) : T := match i with end.
|
||||
|
||||
Definition shift {n : nat} : ren n (S n) :=
|
||||
Some.
|
||||
|
||||
(** Extension of Finite Mappings
|
||||
Assume we are given a mapping _f_ from _I^n_ to some type _X_, then we can _extend_ this mapping with a new value from _x : X_ to a mapping from _I^n+1_ to _X_. We denote this operation by _x . f_ and define it as follows:
|
||||
*)
|
||||
Definition scons {X : Type} {n : nat} (x : X) (f : fin n -> X) (m : fin (S n)) : X :=
|
||||
match m with
|
||||
| None => x
|
||||
| Some i => f i
|
||||
end.
|
||||
|
||||
#[ export ]
|
||||
Hint Opaque scons : rewrite.
|
||||
|
||||
(** ** Type Class Instances for Notation *)
|
||||
|
||||
(** *** 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.
|
||||
|
||||
|
||||
(** ** Proofs for substitution primitives *)
|
||||
|
||||
(** Forward Function Composition
|
||||
Substitutions represented as functions are ubiquitious in this development and we often have to compose them, without talking about their pointwise behaviour.
|
||||
That is, we are interested in the forward compostion of functions, _f o g_, for which we introduce a convenient notation, "f >> g". The direction of the arrow serves as a reminder of the _forward_ nature of this composition, that is first apply _f_, then _g_. *)
|
||||
|
||||
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.
|
||||
|
||||
|
||||
(** Generic lifting operation for renamings *)
|
||||
Definition up_ren {m n} (xi : ren m n) : ren (S m) (S n) :=
|
||||
var_zero .: xi >> shift.
|
||||
|
||||
(** Generic proof that lifting of renamings composes. *)
|
||||
Lemma up_ren_ren k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) :
|
||||
forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
|
||||
Proof.
|
||||
intros [x|].
|
||||
- cbn. unfold funcomp. now rewrite <- E.
|
||||
- reflexivity.
|
||||
Qed.
|
||||
|
||||
Arguments up_ren_ren {k l m} xi zeta rho E.
|
||||
|
||||
Lemma fin_eta {X} (f g : fin 0 -> X) :
|
||||
pointwise_relation _ eq f g.
|
||||
Proof. intros []. Qed.
|
||||
|
||||
(** Eta laws *)
|
||||
Lemma scons_eta' {T} {n : nat} (f : fin (S n) -> T) :
|
||||
pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
|
||||
Proof. intros x. destruct x; reflexivity. Qed.
|
||||
|
||||
Lemma scons_eta_id' {n : nat} :
|
||||
pointwise_relation (fin (S n)) eq (var_zero .: shift) id.
|
||||
Proof. intros x. destruct x; reflexivity. Qed.
|
||||
|
||||
Lemma scons_comp' {T:Type} {U} {m} (s: T) (sigma: fin m -> T) (tau: T -> U) :
|
||||
pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
|
||||
Proof. intros x. destruct x; reflexivity. Qed.
|
||||
|
||||
(* Lemma scons_tail'_pointwise {X} {n} (s : X) (f : fin n -> X) : *)
|
||||
(* pointwise_relation _ eq (funcomp (scons s f) shift) f. *)
|
||||
(* Proof. *)
|
||||
(* reflexivity. *)
|
||||
(* Qed. *)
|
||||
|
||||
(* Lemma scons_tail' {X} {n} (s : X) (f : fin n -> X) x : *)
|
||||
(* (scons s f (shift x)) = f x. *)
|
||||
(* Proof. *)
|
||||
(* reflexivity. *)
|
||||
(* Qed. *)
|
||||
|
||||
(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
|
||||
#[export] Instance scons_morphism {X: Type} {n:nat} :
|
||||
Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X n).
|
||||
Proof.
|
||||
intros t t' -> sigma tau H.
|
||||
intros [x|].
|
||||
cbn. apply H.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
#[export] Instance scons_morphism2 {X: Type} {n: nat} :
|
||||
Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X n).
|
||||
Proof.
|
||||
intros ? t -> sigma tau H ? x ->.
|
||||
destruct x as [x|].
|
||||
cbn. apply H.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(** ** Variadic Substitution Primitives *)
|
||||
|
||||
Fixpoint shift_p (p : nat) {n} : ren n (p + n) :=
|
||||
fun n => match p with
|
||||
| 0 => n
|
||||
| S p => Some (shift_p p n)
|
||||
end.
|
||||
|
||||
Fixpoint scons_p {X: Type} {m : nat} : forall {n} (f : fin m -> X) (g : fin n -> X), fin (m + n) -> X.
|
||||
Proof.
|
||||
destruct m.
|
||||
- intros n f g. exact g.
|
||||
- intros n f g. cbn. apply scons.
|
||||
+ exact (f var_zero).
|
||||
+ apply scons_p.
|
||||
* intros z. exact (f (Some z)).
|
||||
* exact g.
|
||||
Defined.
|
||||
|
||||
#[export] Hint Opaque scons_p : rewrite.
|
||||
|
||||
#[export] Instance scons_p_morphism {X: Type} {m n:nat} :
|
||||
Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons_p X m n).
|
||||
Proof.
|
||||
intros sigma sigma' Hsigma tau tau' Htau.
|
||||
intros x.
|
||||
induction m.
|
||||
- cbn. apply Htau.
|
||||
- cbn. change (fin (S m + n)) with (fin (S (m + n))) in x.
|
||||
destruct x as [x|].
|
||||
+ cbn. apply IHm.
|
||||
intros ?. apply Hsigma.
|
||||
+ cbn. apply Hsigma.
|
||||
Qed.
|
||||
|
||||
#[export] Instance scons_p_morphism2 {X: Type} {m n:nat} :
|
||||
Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons_p X m n).
|
||||
Proof.
|
||||
intros sigma sigma' Hsigma tau tau' Htau ? x ->.
|
||||
induction m.
|
||||
- cbn. apply Htau.
|
||||
- cbn. change (fin (S m + n)) with (fin (S (m + n))) in x.
|
||||
destruct x as [x|].
|
||||
+ cbn. apply IHm.
|
||||
intros ?. apply Hsigma.
|
||||
+ cbn. apply Hsigma.
|
||||
Qed.
|
||||
|
||||
Definition zero_p {m : nat} {n} : fin m -> fin (m + n).
|
||||
Proof.
|
||||
induction m.
|
||||
- intros [].
|
||||
- intros [x|].
|
||||
+ exact (shift_p 1 (IHm x)).
|
||||
+ exact var_zero.
|
||||
Defined.
|
||||
|
||||
Lemma scons_p_head' {X} {m n} (f : fin m -> X) (g : fin n -> X) z:
|
||||
(scons_p f g) (zero_p z) = f z.
|
||||
Proof.
|
||||
induction m.
|
||||
- inversion z.
|
||||
- destruct z.
|
||||
+ simpl. simpl. now rewrite IHm.
|
||||
+ reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma scons_p_head_pointwise {X} {m n} (f : fin m -> X) (g : fin n -> X) :
|
||||
pointwise_relation _ eq (funcomp (scons_p f g) zero_p) f.
|
||||
Proof.
|
||||
intros z.
|
||||
unfold funcomp.
|
||||
induction m.
|
||||
- inversion z.
|
||||
- destruct z.
|
||||
+ simpl. now rewrite IHm.
|
||||
+ reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma scons_p_tail' X m n (f : fin m -> X) (g : fin n -> X) z :
|
||||
scons_p f g (shift_p m z) = g z.
|
||||
Proof. induction m; cbn; eauto. Qed.
|
||||
|
||||
Lemma scons_p_tail_pointwise X m n (f : fin m -> X) (g : fin n -> X) :
|
||||
pointwise_relation _ eq (funcomp (scons_p f g) (shift_p m)) g.
|
||||
Proof. intros z. induction m; cbn; eauto. Qed.
|
||||
|
||||
Lemma destruct_fin {m n} (x : fin (m + n)):
|
||||
(exists x', x = zero_p x') \/ exists x', x = shift_p m x'.
|
||||
Proof.
|
||||
induction m; simpl in *.
|
||||
- right. eauto.
|
||||
- destruct x as [x|].
|
||||
+ destruct (IHm x) as [[x' ->] |[x' ->]].
|
||||
* left. now exists (Some x').
|
||||
* right. eauto.
|
||||
+ left. exists None. eauto.
|
||||
Qed.
|
||||
|
||||
Lemma scons_p_comp' X Y m n (f : fin m -> X) (g : fin n -> X) (h : X -> Y) :
|
||||
pointwise_relation _ eq (funcomp h (scons_p f g)) (scons_p (f >> h) (g >> h)).
|
||||
Proof.
|
||||
intros x.
|
||||
destruct (destruct_fin x) as [[x' ->]|[x' ->]].
|
||||
(* TODO better way to solve this? *)
|
||||
- revert x'.
|
||||
apply pointwise_forall.
|
||||
change (fun x => (scons_p f g >> h) (zero_p x)) with (zero_p >> scons_p f g >> h).
|
||||
now setoid_rewrite scons_p_head_pointwise.
|
||||
- revert x'.
|
||||
apply pointwise_forall.
|
||||
change (fun x => (scons_p f g >> h) (shift_p m x)) with (shift_p m >> scons_p f g >> h).
|
||||
change (fun x => scons_p (f >> h) (g >> h) (shift_p m x)) with (shift_p m >> scons_p (f >> h) (g >> h)).
|
||||
now rewrite !scons_p_tail_pointwise.
|
||||
Qed.
|
||||
|
||||
|
||||
Lemma scons_p_congr {X} {m n} (f f' : fin m -> X) (g g': fin n -> X) z:
|
||||
(forall x, f x = f' x) -> (forall x, g x = g' x) -> scons_p f g z = scons_p f' g' z.
|
||||
Proof. intros H1 H2. induction m; eauto. cbn. destruct z; eauto. Qed.
|
||||
|
||||
(** Generic n-ary lifting operation. *)
|
||||
Definition upRen_p p { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : fin (p + m) -> fin (p + n) :=
|
||||
scons_p (zero_p ) (xi >> shift_p _).
|
||||
|
||||
Arguments upRen_p p {m n} xi.
|
||||
|
||||
(** Generic proof for composition of n-ary lifting. *)
|
||||
Lemma up_ren_ren_p p k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) :
|
||||
forall x, (upRen_p p xi >> upRen_p p zeta) x = upRen_p p rho x.
|
||||
Proof.
|
||||
intros x. destruct (destruct_fin x) as [[? ->]|[? ->]].
|
||||
- unfold upRen_p. unfold funcomp. now repeat rewrite scons_p_head'.
|
||||
- unfold upRen_p. unfold funcomp. repeat rewrite scons_p_tail'.
|
||||
now rewrite <- E.
|
||||
Qed.
|
||||
|
||||
|
||||
Arguments zero_p m {n}.
|
||||
Arguments scons_p {X} m {n} f g.
|
||||
|
||||
Lemma scons_p_eta {X} {m n} {f : fin m -> X}
|
||||
{g : fin n -> X} (h: fin (m + n) -> X) {z: fin (m + n)}:
|
||||
(forall x, g x = h (shift_p m x)) -> (forall x, f x = h (zero_p m x)) -> scons_p m f g z = h z.
|
||||
Proof.
|
||||
intros H1 H2. destruct (destruct_fin z) as [[? ->] |[? ->]].
|
||||
- rewrite scons_p_head'. eauto.
|
||||
- rewrite scons_p_tail'. eauto.
|
||||
Qed.
|
||||
|
||||
Arguments scons_p_eta {X} {m n} {f g} h {z}.
|
||||
Arguments scons_p_congr {X} {m n} {f f'} {g g'} {z}.
|
||||
|
||||
(** ** Notations for Scoped Syntax *)
|
||||
|
||||
Module ScopedNotations.
|
||||
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 ScopedNotations.
|
||||
|
||||
|
||||
(** ** Tactics for Scoped Syntax *)
|
||||
|
||||
Tactic Notation "auto_case" tactic(t) := (match goal with
|
||||
| [|- forall (i : fin 0), _] => intros []; t
|
||||
| [|- forall (i : fin (S (S (S (S _))))), _] => intros [[[[|]|]|]|]; t
|
||||
| [|- forall (i : fin (S (S (S _)))), _] => intros [[[|]|]|]; t
|
||||
| [|- forall (i : fin (S (S _))), _] => intros [[?|]|]; t
|
||||
| [|- forall (i : fin (S _)), _] => intros [?|]; t
|
||||
end).
|
||||
|
||||
#[export] Hint Rewrite @scons_p_head' @scons_p_tail' : FunctorInstances.
|
||||
|
||||
(** 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)) (* AsimplComp *)
|
||||
(* | [|- zero_p >> scons_p ?f ?g] => rewrite scons_p_head *)
|
||||
| [|- context[(?s .: ?sigma) var_zero]] => change ((s.:sigma) var_zero) with s
|
||||
| [|- context[(?s .: ?sigma) (shift ?m)]] => change ((s.:sigma) (shift m)) with (sigma m)
|
||||
(* first [progress setoid_rewrite scons_tail' | progress setoid_rewrite scons_tail'_pointwise ] *)
|
||||
| [|- context[idren >> ?f]] => change (idren >> f) with f
|
||||
| [|- context[?f >> idren]] => change (f >> idren) with f
|
||||
| [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
|
||||
| [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f); eta_reduce
|
||||
| [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite scons_eta'; eta_reduce
|
||||
| [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
|
||||
| [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
|
||||
| [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
|
||||
| [|- context[funcomp _ (scons_p _ _ _)]] => setoid_rewrite scons_p_comp'; eta_reduce
|
||||
| [|- context[scons (@var_zero _) shift]] => setoid_rewrite scons_eta_id'; eta_reduce
|
||||
(* | _ => progress autorewrite with FunctorInstances *)
|
||||
| [|- context[funcomp (scons_p _ _ _) (zero_p _)]] =>
|
||||
first [progress setoid_rewrite scons_p_head_pointwise | progress setoid_rewrite scons_p_head' ]
|
||||
| [|- context[scons_p _ _ _ (zero_p _ _)]] => setoid_rewrite scons_p_head'
|
||||
| [|- context[funcomp (scons_p _ _ _) (shift_p _)]] =>
|
||||
first [progress setoid_rewrite scons_p_tail_pointwise | progress setoid_rewrite scons_p_tail' ]
|
||||
| [|- context[scons_p _ _ _ (shift_p _ _)]] => setoid_rewrite scons_p_tail'
|
||||
| _ => first [progress minimize | progress cbn [shift scons scons_p] ]
|
||||
end.
|
||||
File diff suppressed because it is too large
Load diff
213
theories/Autosubst2/unscoped.v
Normal file
213
theories/Autosubst2/unscoped.v
Normal file
|
|
@ -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.
|
||||
|
|
@ -4,6 +4,7 @@ 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) :=
|
||||
forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
|
||||
|
||||
|
|
|
|||
|
|
@ -1,58 +1,221 @@
|
|||
From Equations Require Import Equations.
|
||||
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
|
||||
common typing preservation admissible fp_red structural soundness.
|
||||
Require Import algorithmic.
|
||||
From stdpp Require Import relations (rtc(..), nsteps(..)).
|
||||
Require Import ssreflect ssrbool.
|
||||
Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax.
|
||||
Derive NoConfusion for option sig nat PTag BTag PTm.
|
||||
Derive EqDec for BTag PTag PTm.
|
||||
Import Logic (inspect).
|
||||
Require Import Cdcl.Itauto.
|
||||
|
||||
Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
|
||||
Require Import ssreflect ssrbool.
|
||||
From Hammer Require Import Tactics.
|
||||
|
||||
Definition ishf (a : PTm) :=
|
||||
match a with
|
||||
| PPair _ _ => true
|
||||
| PAbs _ => true
|
||||
| PUniv _ => true
|
||||
| PBind _ _ _ => true
|
||||
| PNat => true
|
||||
| PSuc _ => true
|
||||
| PZero => true
|
||||
| _ => false
|
||||
end.
|
||||
|
||||
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.
|
||||
|
||||
Module HRed.
|
||||
Inductive R : PTm -> PTm -> Prop :=
|
||||
(****************** Beta ***********************)
|
||||
| AppAbs a b :
|
||||
R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a)
|
||||
|
||||
| ProjPair p a b :
|
||||
R (PProj p (PPair a b)) (if p is PL then a else b)
|
||||
|
||||
| IndZero P b c :
|
||||
R (PInd P PZero b c) b
|
||||
|
||||
| IndSuc P a b c :
|
||||
R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
|
||||
|
||||
(*************** Congruence ********************)
|
||||
| AppCong a0 a1 b :
|
||||
R a0 a1 ->
|
||||
R (PApp a0 b) (PApp a1 b)
|
||||
| ProjCong p a0 a1 :
|
||||
R a0 a1 ->
|
||||
R (PProj p a0) (PProj p a1)
|
||||
| IndCong P a0 a1 b c :
|
||||
R a0 a1 ->
|
||||
R (PInd P a0 b c) (PInd P a1 b c).
|
||||
|
||||
Definition nf a := forall b, ~ R a b.
|
||||
End HRed.
|
||||
|
||||
|
||||
Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false.
|
||||
|
||||
Definition isuniv (a : PTm) := if a is PUniv _ then true else false.
|
||||
|
||||
Definition ispair (a : PTm) :=
|
||||
match a with
|
||||
| PPair _ _ => true
|
||||
| _ => false
|
||||
end.
|
||||
|
||||
Definition isnat (a : PTm) := if a is PNat then true else false.
|
||||
|
||||
Definition iszero (a : PTm) := if a is PZero then true else false.
|
||||
|
||||
Definition issuc (a : PTm) := if a is PSuc _ then true else false.
|
||||
|
||||
Definition isabs (a : PTm) :=
|
||||
match a with
|
||||
| PAbs _ => true
|
||||
| _ => false
|
||||
end.
|
||||
|
||||
Definition tm_nonconf (a b : PTm) : bool :=
|
||||
match a, b with
|
||||
| PAbs _, _ => ishne b || isabs b
|
||||
| _, PAbs _ => ishne a
|
||||
| VarPTm _, VarPTm _ => true
|
||||
| PPair _ _, _ => ishne b || ispair b
|
||||
| _, PPair _ _ => ishne a
|
||||
| PZero, PZero => true
|
||||
| PSuc _, PSuc _ => true
|
||||
| PApp _ _, PApp _ _ => ishne a && ishne b
|
||||
| PProj _ _, PProj _ _ => ishne a && ishne b
|
||||
| PInd _ _ _ _, PInd _ _ _ _ => ishne a && ishne b
|
||||
| PNat, PNat => true
|
||||
| PUniv _, PUniv _ => true
|
||||
| PBind _ _ _, PBind _ _ _ => true
|
||||
| _,_=> false
|
||||
end.
|
||||
|
||||
Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
|
||||
|
||||
Inductive eq_view : PTm -> PTm -> Type :=
|
||||
| V_AbsAbs a b :
|
||||
eq_view (PAbs a) (PAbs b)
|
||||
| V_AbsNeu a b :
|
||||
~~ isabs b ->
|
||||
eq_view (PAbs a) b
|
||||
| V_NeuAbs a b :
|
||||
~~ isabs a ->
|
||||
eq_view a (PAbs b)
|
||||
| V_VarVar i j :
|
||||
eq_view (VarPTm i) (VarPTm j)
|
||||
| V_PairPair a0 b0 a1 b1 :
|
||||
eq_view (PPair a0 b0) (PPair a1 b1)
|
||||
| V_PairNeu a0 b0 u :
|
||||
~~ ispair u ->
|
||||
eq_view (PPair a0 b0) u
|
||||
| V_NeuPair u a1 b1 :
|
||||
~~ ispair u ->
|
||||
eq_view u (PPair a1 b1)
|
||||
| V_ZeroZero :
|
||||
eq_view PZero PZero
|
||||
| V_SucSuc a b :
|
||||
eq_view (PSuc a) (PSuc b)
|
||||
| V_AppApp u0 b0 u1 b1 :
|
||||
eq_view (PApp u0 b0) (PApp u1 b1)
|
||||
| V_ProjProj p0 u0 p1 u1 :
|
||||
eq_view (PProj p0 u0) (PProj p1 u1)
|
||||
| V_IndInd P0 u0 b0 c0 P1 u1 b1 c1 :
|
||||
eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
|
||||
| V_NatNat :
|
||||
eq_view PNat PNat
|
||||
| V_BindBind p0 A0 B0 p1 A1 B1 :
|
||||
eq_view (PBind p0 A0 B0) (PBind p1 A1 B1)
|
||||
| V_UnivUniv i j :
|
||||
eq_view (PUniv i) (PUniv j)
|
||||
| V_Others a b :
|
||||
eq_view a b.
|
||||
|
||||
Equations tm_to_eq_view (a b : PTm) : eq_view a b :=
|
||||
tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b;
|
||||
tm_to_eq_view (PAbs a) b := V_AbsNeu a b _;
|
||||
tm_to_eq_view a (PAbs b) := V_NeuAbs a b _;
|
||||
tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j;
|
||||
tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1;
|
||||
tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _;
|
||||
tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _;
|
||||
tm_to_eq_view PZero PZero := V_ZeroZero;
|
||||
tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b;
|
||||
tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1;
|
||||
tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1;
|
||||
tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1;
|
||||
tm_to_eq_view PNat PNat := V_NatNat;
|
||||
tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j;
|
||||
tm_to_eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1;
|
||||
tm_to_eq_view a b := V_Others a b.
|
||||
|
||||
Inductive algo_dom : PTm -> PTm -> Prop :=
|
||||
| A_AbsAbs a b :
|
||||
algo_dom a b ->
|
||||
algo_dom_r a b ->
|
||||
(* --------------------- *)
|
||||
algo_dom (PAbs a) (PAbs b)
|
||||
|
||||
| A_AbsNeu a u :
|
||||
ishne u ->
|
||||
algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
|
||||
algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
|
||||
(* --------------------- *)
|
||||
algo_dom (PAbs a) u
|
||||
|
||||
| A_NeuAbs a u :
|
||||
ishne u ->
|
||||
algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
|
||||
algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
|
||||
(* --------------------- *)
|
||||
algo_dom u (PAbs a)
|
||||
|
||||
| A_PairPair a0 a1 b0 b1 :
|
||||
algo_dom a0 a1 ->
|
||||
algo_dom b0 b1 ->
|
||||
algo_dom_r a0 a1 ->
|
||||
algo_dom_r b0 b1 ->
|
||||
(* ---------------------------- *)
|
||||
algo_dom (PPair a0 b0) (PPair a1 b1)
|
||||
|
||||
| A_PairNeu a0 a1 u :
|
||||
ishne u ->
|
||||
algo_dom a0 (PProj PL u) ->
|
||||
algo_dom a1 (PProj PR u) ->
|
||||
algo_dom_r a0 (PProj PL u) ->
|
||||
algo_dom_r a1 (PProj PR u) ->
|
||||
(* ----------------------- *)
|
||||
algo_dom (PPair a0 a1) u
|
||||
|
||||
| A_NeuPair a0 a1 u :
|
||||
ishne u ->
|
||||
algo_dom (PProj PL u) a0 ->
|
||||
algo_dom (PProj PR u) a1 ->
|
||||
algo_dom_r (PProj PL u) a0 ->
|
||||
algo_dom_r (PProj PR u) a1 ->
|
||||
(* ----------------------- *)
|
||||
algo_dom u (PPair a0 a1)
|
||||
|
||||
| A_ZeroZero :
|
||||
algo_dom PZero PZero
|
||||
|
||||
| A_SucSuc a0 a1 :
|
||||
algo_dom_r a0 a1 ->
|
||||
algo_dom (PSuc a0) (PSuc a1)
|
||||
|
||||
| A_UnivCong i j :
|
||||
(* -------------------------- *)
|
||||
algo_dom (PUniv i) (PUniv j)
|
||||
|
||||
| A_BindCong p0 p1 A0 A1 B0 B1 :
|
||||
algo_dom A0 A1 ->
|
||||
algo_dom B0 B1 ->
|
||||
algo_dom_r A0 A1 ->
|
||||
algo_dom_r B0 B1 ->
|
||||
(* ---------------------------- *)
|
||||
algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
|
||||
|
||||
| A_NatCong :
|
||||
algo_dom PNat PNat
|
||||
|
||||
| A_VarCong i j :
|
||||
(* -------------------------- *)
|
||||
algo_dom (VarPTm i) (VarPTm j)
|
||||
|
|
@ -68,78 +231,199 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
|
|||
ishne u0 ->
|
||||
ishne u1 ->
|
||||
algo_dom u0 u1 ->
|
||||
algo_dom a0 a1 ->
|
||||
algo_dom_r a0 a1 ->
|
||||
(* ------------------------- *)
|
||||
algo_dom (PApp u0 a0) (PApp u1 a1)
|
||||
|
||||
| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
|
||||
ishne u0 ->
|
||||
ishne u1 ->
|
||||
algo_dom_r P0 P1 ->
|
||||
algo_dom u0 u1 ->
|
||||
algo_dom_r b0 b1 ->
|
||||
algo_dom_r c0 c1 ->
|
||||
algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
|
||||
|
||||
with algo_dom_r : PTm -> PTm -> Prop :=
|
||||
| A_NfNf a b :
|
||||
algo_dom a b ->
|
||||
algo_dom_r a b
|
||||
|
||||
| A_HRedL a a' b :
|
||||
HRed.R a a' ->
|
||||
algo_dom a' b ->
|
||||
algo_dom_r a' b ->
|
||||
(* ----------------------- *)
|
||||
algo_dom a b
|
||||
algo_dom_r a b
|
||||
|
||||
| A_HRedR a b b' :
|
||||
ishne a \/ ishf a ->
|
||||
HRed.R b b' ->
|
||||
algo_dom a b' ->
|
||||
algo_dom_r a b' ->
|
||||
(* ----------------------- *)
|
||||
algo_dom a b.
|
||||
algo_dom_r a b.
|
||||
|
||||
|
||||
Definition fin_eq {n} (i j : fin n) : bool.
|
||||
Lemma algo_dom_hf_hne (a b : PTm) :
|
||||
algo_dom a b ->
|
||||
(ishf a \/ ishne a) /\ (ishf b \/ ishne b).
|
||||
Proof.
|
||||
induction n.
|
||||
- by exfalso.
|
||||
- refine (match i , j with
|
||||
| None, None => true
|
||||
| Some i, Some j => IHn i j
|
||||
| _, _ => false
|
||||
end).
|
||||
Defined.
|
||||
induction 1 =>//=; hauto lq:on.
|
||||
Qed.
|
||||
|
||||
Lemma fin_eq_dec {n} (i j : fin n) :
|
||||
Bool.reflect (i = j) (fin_eq i j).
|
||||
Lemma hf_no_hred (a b : PTm) :
|
||||
ishf a ->
|
||||
HRed.R a b ->
|
||||
False.
|
||||
Proof. hauto l:on inv:HRed.R. Qed.
|
||||
|
||||
Lemma hne_no_hred (a b : PTm) :
|
||||
ishne a ->
|
||||
HRed.R a b ->
|
||||
False.
|
||||
Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
|
||||
|
||||
Derive Signature for algo_dom algo_dom_r.
|
||||
|
||||
Fixpoint hred (a : PTm) : option (PTm) :=
|
||||
match a with
|
||||
| VarPTm i => None
|
||||
| PAbs a => None
|
||||
| PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a)
|
||||
| PApp a b =>
|
||||
match hred a with
|
||||
| Some a => Some (PApp a b)
|
||||
| None => None
|
||||
end
|
||||
| PPair a b => None
|
||||
| PProj p (PPair a b) => if p is PL then Some a else Some b
|
||||
| PProj p a =>
|
||||
match hred a with
|
||||
| Some a => Some (PProj p a)
|
||||
| None => None
|
||||
end
|
||||
| PUniv i => None
|
||||
| PBind p A B => None
|
||||
| PBot => None
|
||||
| PNat => None
|
||||
| PZero => None
|
||||
| PSuc a => None
|
||||
| PInd P PZero b c => Some b
|
||||
| PInd P (PSuc a) b c =>
|
||||
Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
|
||||
| PInd P a b c =>
|
||||
match hred a with
|
||||
| Some a => Some (PInd P a b c)
|
||||
| None => None
|
||||
end
|
||||
end.
|
||||
|
||||
Lemma hred_complete (a b : PTm) :
|
||||
HRed.R a b -> hred a = Some b.
|
||||
Proof.
|
||||
revert i j. induction n.
|
||||
- destruct i.
|
||||
- destruct i; destruct j.
|
||||
+ specialize (IHn f f0).
|
||||
inversion IHn; subst.
|
||||
simpl. rewrite -H.
|
||||
apply ReflectT.
|
||||
reflexivity.
|
||||
simpl. rewrite -H.
|
||||
apply ReflectF.
|
||||
injection. tauto.
|
||||
+ by apply ReflectF.
|
||||
+ by apply ReflectF.
|
||||
+ by apply ReflectT.
|
||||
Defined.
|
||||
induction 1; hauto lq:on rew:off inv:HRed.R b:on.
|
||||
Qed.
|
||||
|
||||
Lemma hred_sound (a b : PTm):
|
||||
hred a = Some b -> HRed.R a b.
|
||||
Proof.
|
||||
elim : a b; hauto q:on dep:on ctrs:HRed.R.
|
||||
Qed.
|
||||
|
||||
Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
|
||||
Lemma hred_deter (a b0 b1 : PTm) :
|
||||
HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
|
||||
Proof.
|
||||
move /hred_complete => + /hred_complete. congruence.
|
||||
Qed.
|
||||
|
||||
Ltac check_equal_triv :=
|
||||
intros;subst;
|
||||
lazymatch goal with
|
||||
(* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
|
||||
| [h : algo_dom _ _ |- _] => try (inversion h; by subst)
|
||||
| _ => idtac
|
||||
end.
|
||||
|
||||
Ltac solve_check_equal :=
|
||||
try solve [intros *;
|
||||
match goal with
|
||||
| [|- _ = _] => sauto
|
||||
| _ => idtac
|
||||
end].
|
||||
|
||||
Equations check_equal (a b : PTm) (h : algo_dom a b) :
|
||||
bool by struct h :=
|
||||
check_equal a b h with (@idP (ishne a || ishf a)) := {
|
||||
| Bool.ReflectT _ _ => _
|
||||
| Bool.ReflectF _ _ => _
|
||||
}.
|
||||
check_equal a b h with tm_to_eq_view a b :=
|
||||
check_equal _ _ h (V_VarVar i j) := nat_eqdec i j;
|
||||
check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_PairPair a0 b0 a1 b1) :=
|
||||
check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_PairNeu a0 b0 u _) :=
|
||||
check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_NeuPair u a1 b1 _) :=
|
||||
check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv);
|
||||
check_equal _ _ h V_NatNat := true;
|
||||
check_equal _ _ h V_ZeroZero := true;
|
||||
check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_ProjProj p0 a p1 b) :=
|
||||
PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_AppApp a0 b0 a1 b1) :=
|
||||
check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) :=
|
||||
check_equal_r P0 P1 ltac:(check_equal_triv) &&
|
||||
check_equal u0 u1 ltac:(check_equal_triv) &&
|
||||
check_equal_r b0 b1 ltac:(check_equal_triv) &&
|
||||
check_equal_r c0 c1 ltac:(check_equal_triv);
|
||||
check_equal _ _ h (V_UnivUniv i j) := Nat.eqb i j;
|
||||
check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) :=
|
||||
BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv);
|
||||
check_equal _ _ _ _ := false
|
||||
|
||||
(* check_equal a b h := false; *)
|
||||
with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) :
|
||||
bool by struct h0 :=
|
||||
check_equal_r a b h with inspect (hred a) :=
|
||||
check_equal_r a b h (exist _ (Some a') k) := check_equal_r a' b _;
|
||||
check_equal_r a b h (exist _ None k) with inspect (hred b) :=
|
||||
| (exist _ None l) => tm_nonconf a b && check_equal a b _;
|
||||
| (exist _ (Some b') l) => check_equal_r a b' _.
|
||||
|
||||
(* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *)
|
||||
(* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *)
|
||||
(* check_equal (PPair a0 b0) (PPair a1 b1) h := *)
|
||||
(* check_equal a0 b0 _ && check_equal a1 b1 _; *)
|
||||
(* check_equal (PUniv i) (PUniv j) _ := _; *)
|
||||
Next Obligation.
|
||||
simpl.
|
||||
intros ih.
|
||||
Admitted.
|
||||
intros.
|
||||
destruct h.
|
||||
exfalso. apply algo_dom_hf_hne in H.
|
||||
apply hred_sound in k.
|
||||
destruct H as [[|] _].
|
||||
eauto using hf_no_hred.
|
||||
eauto using hne_no_hred.
|
||||
apply hred_sound in k.
|
||||
assert ( a'0 = a')by eauto using hred_deter. subst.
|
||||
apply h.
|
||||
exfalso.
|
||||
apply hred_sound in k.
|
||||
destruct H as [|].
|
||||
eauto using hne_no_hred.
|
||||
eauto using hf_no_hred.
|
||||
Defined.
|
||||
|
||||
Search (Bool.reflect (is_true _) _).
|
||||
Check idP.
|
||||
Next Obligation.
|
||||
simpl. intros.
|
||||
inversion h; subst =>//=.
|
||||
move {h}. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound.
|
||||
apply False_ind. hauto l:on use:hred_complete.
|
||||
assert (b' = b'0) by eauto using hred_deter, hred_sound.
|
||||
subst.
|
||||
assumption.
|
||||
Defined.
|
||||
|
||||
Definition metric {n} k (a b : PTm n) :=
|
||||
exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\
|
||||
nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
|
||||
Next Obligation.
|
||||
intros.
|
||||
inversion h; subst => //=.
|
||||
exfalso. hauto l:on use:hred_complete.
|
||||
exfalso. hauto l:on use:hred_complete.
|
||||
Defined.
|
||||
|
||||
Search (nat -> nat -> bool).
|
||||
Next Obligation.
|
||||
qauto inv:algo_dom, algo_dom_r.
|
||||
Defined.
|
||||
(* Do not step back from here or otherwise equations will cause an error *)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue