From 11bfed2d17f48715b7a442f6bccd52b2a75b54a9 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 00:30:02 -0500 Subject: [PATCH] Finish defining the algorithm --- Makefile | 2 +- theories/Autosubst2/fintype.v | 419 ---------------------------------- theories/Autosubst2/syntax.v | 10 +- theories/executable.v | 125 ++++++---- 4 files changed, 84 insertions(+), 472 deletions(-) delete mode 100644 theories/Autosubst2/fintype.v diff --git a/Makefile b/Makefile index 3c879f6..972974b 100644 --- a/Makefile +++ b/Makefile @@ -22,6 +22,6 @@ theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fint 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: diff --git a/theories/Autosubst2/fintype.v b/theories/Autosubst2/fintype.v deleted file mode 100644 index 99508b6..0000000 --- a/theories/Autosubst2/fintype.v +++ /dev/null @@ -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. diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 3d1e1f6..97ebfb1 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -711,11 +711,11 @@ Qed. Class Up_PTm X Y := up_PTm : X -> Y. -#[global]Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm. +#[global] Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm. -#[global]Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm. +#[global] Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm. -#[global]Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm. +#[global] Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm. #[global] Instance VarInstance_PTm : (Var _ _) := @VarPTm. @@ -833,9 +833,9 @@ Module Extra. Import Core. -#[global]Hint Opaque subst_PTm: rewrite. +#[global] Hint Opaque subst_PTm: rewrite. -#[global]Hint Opaque ren_PTm: rewrite. +#[global] Hint Opaque ren_PTm: rewrite. End Extra. diff --git a/theories/executable.v b/theories/executable.v index b4dcfbe..69e6d78 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -1,6 +1,7 @@ From Equations Require Import Equations. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. -Derive NoConfusion for sig option nat PTag BTag PTm. +Derive NoConfusion for sig nat PTag BTag PTm. +Derive EqDec for BTag PTag PTm. Import Logic (inspect). Require Import ssreflect ssrbool. @@ -97,6 +98,13 @@ Inductive algo_dom : PTm -> PTm -> Prop := (* ----------------------- *) 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) @@ -107,6 +115,9 @@ Inductive algo_dom : PTm -> PTm -> Prop := (* ---------------------------- *) 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) @@ -126,6 +137,15 @@ Inductive algo_dom : PTm -> PTm -> Prop := (* ------------------------- *) 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 -> @@ -164,23 +184,6 @@ Lemma hne_no_hred (a b : PTm) : Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. Derive Signature for algo_dom algo_dom_r. -(* Fixpoint PTm_eqb {n} (a b : PTm n) := *) -(* match a, b with *) -(* | VarPTm i, VarPTm j => fin_eq i j *) -(* | PAbs a, PAbs b => PTm_eqb a b *) -(* | PApp a0 b0, PApp a1 b1 => PTm_eqb a0 a1 && PTm_eqb b0 b1 *) -(* | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_beq p0 p1 && PTm_eqb A0 A1 && PTm_eqb B0 B1 *) -(* | PPair a0 b0, PPair a1 b1 => PTm_eqb a0 a1 && PTm_eqb b0 b1 *) -(* | *) - -(* Lemma hred {n} (a : PTm n) : (relations.nf HRed.R a) + {x | HRed.R a x}. *) -(* Proof. *) -(* induction a. *) -(* - hauto lq:on inv:HRed.R unfold:relations.nf. *) -(* - hauto lq:on inv:HRed.R unfold:relations.nf. *) -(* - clear IHa2. *) -(* destruct IHa1. *) -(* destruct a1. *) Fixpoint hred (a : PTm) : option (PTm) := match a with @@ -262,8 +265,6 @@ Ltac check_equal_triv := | _ => idtac end. -Scheme Equality for nat. Scheme Equality for PTag. -Scheme Equality for BTag. Scheme Equality for PTm. (* Program Fixpoint check_equal {n} (a b : PTm n) (h : algo_dom a b) {struct h} : bool := *) (* match a, b with *) (* | VarPTm i, VarPTm j => fin_beq i j *) @@ -278,24 +279,44 @@ Scheme Equality for BTag. Scheme Equality for PTm. (* Next Obligation. *) (* simpl. *) + +Ltac solve_check_equal := + try solve [intros *; + match goal with + | [|- _ = _] => sauto + | _ => idtac + end]. + +(* #[export,global] Obligation Tactic := idtac "fiewof". *) + + Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := - (* check_equal (VarPTm i) (VarPTm j) h := nat_beq i j; *) - (* check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); *) - (* check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); *) - (* check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); *) - (* check_equal (PPair a0 b0) (PPair a1 b1) h := *) - (* check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); *) - (* check_equal (PPair a0 b0) u h := *) - (* check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); *) - (* check_equal u (PPair a1 b1) h := *) - (* check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); *) - (* check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := *) - (* BTag_beq p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); *) - (* check_equal PNat PNat _ := true; *) - (* check_equal PZero PZero _ := true; *) - (* check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); *) - (* check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; *) + check_equal (VarPTm i) (VarPTm j) h := nat_eqdec i j; + check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); + check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); + check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); + check_equal (PPair a0 b0) (PPair a1 b1) h := + check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal (PPair a0 b0) u h := + check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); + check_equal u (PPair a1 b1) h := + check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); + check_equal PNat PNat _ := true; + check_equal PZero PZero _ := true; + check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); + check_equal (PProj p0 a) (PProj p1 b) h := + PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); + check_equal (PApp a0 b0) (PApp a1 b1) h := + check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) h := + 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 (PUniv i) (PUniv j) _ := Nat.eqb i j; + check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := + BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); check_equal a b h := false; with check_equal_r (a b : PTm) (h : algo_dom_r a b) : bool by struct h := @@ -306,30 +327,40 @@ Equations check_equal (a b : PTm) (h : algo_dom a b) : | (exist _ (Some b') l) => check_equal_r a b' _}} . Next Obligation. - simpl. - inversion h; subst =>//=. - exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. - suff ? : a'0 = a' by subst; assumption. - by eauto using hred_deter, hred_sound. - exfalso. hauto lq:on use:hf_no_hred, hne_no_hred, hred_sound. + 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. Next Obligation. - simpl. + simpl. intros. inversion h; subst =>//=. - exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. - exfalso. hauto l:on use:hred_complete. - have ? : b' = b'0 by eauto using hred_deter, hred_sound. + 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. Next Obligation. + intros. inversion h; subst => //=. exfalso. hauto l:on use:hred_complete. exfalso. hauto l:on use:hred_complete. Defined. Next Obligation. - sauto lq:on. + sauto. Defined.