From 580e3a8251d69288623adfe8368987f246c49f24 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Fri, 31 Jan 2025 20:54:33 -0500
Subject: [PATCH] Prove that ered is strongly normalizing

---
 theories/fp_red.v | 35 +++++++++++++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 0ca4dfe..aa9b111 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -4,9 +4,9 @@ Import Ltac2.Notations.
 Import Ltac2.Control.
 Require Import ssreflect ssrbool.
 Require Import FunInd.
-Require Import Arith.Wf_nat.
+Require Import Arith.Wf_nat (well_founded_lt_compat).
 Require Import Psatz.
-From stdpp Require Import relations (rtc (..), rtc_once, rtc_r).
+From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn).
 From Hammer Require Import Tactics.
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
 Require Import Btauto.
@@ -1438,4 +1438,35 @@ Module LoReds.
       have : ~~ ishf a by inversion h.
       hauto lq:on ctrs:LoRed.R.
   Qed.
+
 End LoReds.
+
+
+Fixpoint size_PTm {n} (a : PTm n) :=
+  match a with
+  | VarPTm _ => 1
+  | PAbs a => 1 + size_PTm a
+  | PApp a b => 1 + Nat.add (size_PTm a) (size_PTm b)
+  | PProj p a => 1 + size_PTm a
+  | PPair a b => 1 + Nat.add (size_PTm a) (size_PTm b)
+  end.
+
+Lemma size_PTm_ren n m (ξ : fin n -> fin m) a : size_PTm (ren_PTm ξ a) = size_PTm a.
+Proof.
+  move : m ξ. elim : n / a => //=; scongruence.
+Qed.
+
+#[export]Hint Rewrite size_PTm_ren : sizetm.
+
+Lemma ered_size {n} (a b : PTm n) :
+  ERed.R a b ->
+  size_PTm b < size_PTm a.
+Proof.
+  move => h. elim : n a b /h; hauto l:on rew:db:sizetm.
+Qed.
+
+Lemma ered_sn n (a : PTm n) : sn ERed.R a.
+Proof.
+  hauto lq:on rew:off use:size_PTm_ren, ered_size,
+          well_founded_lt_compat unfold:well_founded.
+Qed.