From b29d567ef034039eaaae5880e086a25afd9f6936 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 5 Mar 2025 00:18:28 -0500 Subject: [PATCH] Add termination --- theories/termination.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 theories/termination.v diff --git a/theories/termination.v b/theories/termination.v new file mode 100644 index 0000000..61f1e1d --- /dev/null +++ b/theories/termination.v @@ -0,0 +1,14 @@ +Require Import common Autosubst2.core Autosubst2.unscoped Autosubst2.syntax algorithmic fp_red executable. +From Hammer Require Import Tactics. +Require Import ssreflect ssrbool. +From stdpp Require Import relations (nsteps (..)). + +Definition term_metric k (a b : PTm) := + 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. + +Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b. +Proof. + elim /Wf_nat.lt_wf_ind. + move => n ih a b h. + case : (fancy_hred a); cycle 1. + move => [a' ha']. apply : A_HRedL; eauto.