From c6edc1b0be3c4be48e511a2cea766c6974b49947 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 24 Dec 2024 01:19:42 -0500 Subject: [PATCH] Add prov function (WIP) --- theories/fp_red.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index e04d509..f753e2c 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -752,6 +752,14 @@ Proof. sfirstorder use:relations.diamond_confluent, EPar_diamond. Qed. +Fixpoint prov {n} A B (a : Tm n) : Prop := + match a with + | Pi A0 B0 => rtc Par.R A A0 /\ rtc Par.R B B0 + | App a b => prov A B a + | Abs a => prov A B (subst_Tm (scons A VarTm) a) + | _ => True + end. + Lemma Par_confluent n (c a1 b1 : Tm n) : rtc Par.R c a1 -> rtc Par.R c b1 ->