From 2af49373e3fa84b8691a791e1538b60b8c1f61ea Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Fri, 21 Feb 2025 15:11:12 -0500
Subject: [PATCH] Repair epar sn preservation

---
 theories/fp_red.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 7068cb1..9ee4595 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -517,6 +517,14 @@ Proof.
   hauto lq:on rew:off inv:TRedSN db:sn.
 Qed.
 
+Lemma SN_IndInv : forall n P (a : PTm n) b c, SN (PInd P a b c) -> SN P /\ SN a /\ SN b /\ SN c.
+Proof.
+  move => n P a b c. move E : (PInd P a b c) => u hu. move : P a b c E.
+  elim  : n u / hu => //=.
+  hauto lq:on rew:off inv:SNe db:sn.
+  hauto lq:on rew:off inv:TRedSN db:sn.
+Qed.
+
 Lemma epar_sn_preservation n :
   (forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\
   (forall (a : PTm n) (s : SN a), forall b, EPar.R a b -> SN b) /\
@@ -527,6 +535,7 @@ Proof.
   - sauto lq:on.
   - sauto lq:on.
   - sauto lq:on.
+  - sauto lq:on.
   - move => a b ha iha hb ihb b0.
     inversion 1; subst.
     + have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
@@ -545,6 +554,9 @@ Proof.
   - sauto lq:on.
   - sauto lq:on.
   - sauto lq:on.
+  - sauto lq:on.
+  - sauto lq:on.
+  - sauto lq:on.
   - move => a b ha iha c h0.
     inversion h0; subst.
     inversion H1; subst.
@@ -576,6 +588,15 @@ Proof.
       sauto lq:on.
     + sauto lq:on.
   - sauto.
+  - sauto q:on.
+  - move => P a b c hP ihP ha iha hb ihb hc ihc u.
+    elim /EPar.inv => //=_.
+    move => P0 P1 a0 a1 b0 b1 c0 c1 hP0 ha0 hb0 hc0 [*]. subst.
+    elim /EPar.inv : ha0 => //=_.
+    move => a0 a2 ha0 [*]. subst.
+    eexists. split. apply T_Once. apply N_IndSuc; eauto.
+    hauto q:on ctrs:EPar.R use:EPar.morphing, EPar.refl inv:option.
+  - sauto q:on.
 Qed.
 
 Module RRed.