From 6c11f5560db3ba1b043430d9815d3e68691754ac Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 27 Feb 2025 20:56:01 -0500 Subject: [PATCH] Need noconfusion? --- theories/executable.v | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 144979d..dd7d2aa 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -93,7 +93,11 @@ with algo_dom_r {n} : PTm n -> PTm n -> Prop := algo_dom_r a b. Derive Signature for algo_dom algo_dom_r. - +Derive NoConfusion for PTm. +Next Obligation. +Admitted. +Next Obligation. +Admitted. Derive Dependent Inversion adom_inv with (forall n (a b : PTm n), algo_dom a b) Sort Prop. @@ -230,22 +234,26 @@ Proof. Defined. 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. -Lemma algo_dom_hne_abs_inv n (a : PTm n) b : - ishne a -> - algo_dom a (PAbs b) -> - algo_dom_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b. -Proof. - remember (PAbs b) as u. - destruct 2; try (exfalso; simpl in *; congruence). - injection Hequ. move => <-. - apply H1. -Defined. +(* 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 *) +(* | PAbs a, PAbs b => check_equal_r a b ltac:(check_equal_triv) *) +(* | _, _ => false *) +(* end *) +(* with check_equal_r {n} (a b : PTm n) (h : algo_dom_r a b) {struct h} : bool := *) +(* match hred_fancy _ a with *) +(* | inr a' => check_equal_r (proj1_sig a') b _ *) +(* | _ => false *) +(* end. *) +(* Next Obligation. *) +(* simpl. *) Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) : bool by struct h :=