open import Graded.Modality
open import Graded.Usage.Restrictions
module Graded.Derived.Sigma
{a} {M : Set a}
(π : Modality M)
(UR : Usage-restrictions M)
where
open Modality π
open Usage-restrictions UR
open import Graded.Context π
open import Graded.Context.Properties π
open import Graded.Modality.Properties π
open import Graded.Usage π UR
open import Graded.Usage.Inversion π UR
open import Graded.Usage.Properties π UR
open import Graded.Usage.Weakening π UR
open import Graded.Substitution.Properties π UR
open import Graded.Mode π
open import Definition.Untyped M
open import Definition.Untyped.Sigma M as Sigma
using (prodrecβ; module Fstα΅£-sndα΅£)
open import Tools.Bool using (T)
open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat; 1+)
open import Tools.Nullary
open import Tools.Product
open import Tools.PropositionalEquality as PE using (_β’_)
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Sum using (_β_; injβ; injβ)
private variable
n : Nat
A B t u : Term _
p q r : M
Ξ³ Ξ΄ : Conβ _
m : Mode
private
πβ°πβπβ§πβ’π : Β¬ π β€ π β π β§ π β’ π
πβ°πβπβ§πβ’π πβ°π =
π β§ π PE.β‘ π ββ¨ flip (PE.subst (_β€ _)) (β§-decreasingΚ³ π π) β©
π β€ π ββ¨ πβ°π β©
β₯ β‘
πβ°πβπβ‘πββ’πα΅βα΅Β·[πβ§π]β‘ :
β m β Β¬ π β€ π β π PE.β‘ π β m β’ πα΅ β m α΅Β· (π β§ π) PE.β‘ m
πβ°πβπβ‘πββ’πα΅βα΅Β·[πβ§π]β‘ = Ξ» where
πα΅ _ β PE.refl
πα΅ πβ°πβπβ‘πββ’πα΅ β case πβ°πβπβ‘πββ’πα΅ of Ξ» where
(injβ πβ°π) β β’πββββ‘πα΅ (πβ°πβπβ§πβ’π πβ°π)
(injβ (injβ πβ‘π)) β Mode-propositional-if-πβ‘π πβ‘π
(injβ (injβ β’πα΅)) β β₯-elim (β’πα΅ PE.refl)
β€πβπβ°πβπβ‘π : π PE.β‘ π β π β’ π β (β p β p β€ π) β Β¬ π β€ π β π PE.β‘ π
β€πβπβ°πβπβ‘π = Ξ» where
(injβ πβ‘π) _ β injβ πβ‘π
(injβ πβ’π) β€π β injβ
(π β€ π ββ¨ β€-antisym (β€π _) β©
π PE.β‘ π ββ¨ πβ’π β©
β₯ β‘)
[πβ§π]Β·αΆβ‘παΆβ§αΆ : (π β§ π) Β·αΆ Ξ³ PE.β‘ παΆ β§αΆ Ξ³
[πβ§π]Β·αΆβ‘παΆβ§αΆ {Ξ³ = Ξ³} =
(π β§ π) Β·αΆ Ξ³ β‘β¨ βαΆββ‘ (Β·αΆ-distribΚ³-β§αΆ _ _ _) β©
π Β·αΆ Ξ³ β§αΆ π Β·αΆ Ξ³ β‘β¨ βαΆββ‘ (β§αΆ-cong (Β·αΆ-zeroΛ‘ _) (Β·αΆ-identityΛ‘ _)) β©
παΆ β§αΆ Ξ³ β
where
open Tools.Reasoning.PropositionalEquality
[πβ§π]Β·β‘πβ§ : (π β§ π) Β· p PE.β‘ π β§ p
[πβ§π]Β·β‘πβ§ {p = p} =
(π β§ π) Β· p β‘β¨ Β·-distribΚ³-β§ _ _ _ β©
π Β· p β§ π Β· p β‘β¨ β§-cong (Β·-zeroΛ‘ _) (Β·-identityΛ‘ _) β©
π β§ p β
where
open Tools.Reasoning.PropositionalEquality
Β·[πβ§π]β‘πβ§ : p Β· (π β§ π) PE.β‘ π β§ p
Β·[πβ§π]β‘πβ§ {p = p} =
p Β· (π β§ π) β‘β¨ Β·-distribΛ‘-β§ _ _ _ β©
p Β· π β§ p Β· π β‘β¨ β§-cong (Β·-zeroΚ³ _) (Β·-identityΚ³ _) β©
π β§ p β
where
open Tools.Reasoning.PropositionalEquality
Β·[πβ§π]Β·β‘πβ§Β· : p Β· (π β§ π) Β· q PE.β‘ π β§ p Β· q
Β·[πβ§π]Β·β‘πβ§Β· {p = p} {q = q} =
p Β· (π β§ π) Β· q β‘β¨ Β·-congΛ‘ [πβ§π]Β·β‘πβ§ β©
p Β· (π β§ q) β‘β¨ Β·-distribΛ‘-β§ _ _ _ β©
p Β· π β§ p Β· q β‘β¨ β§-congΚ³ (Β·-zeroΚ³ _) β©
π β§ p Β· q β
where
open Tools.Reasoning.PropositionalEquality
prodβα΅£β :
(β p q β p + q β€ p β§ q) β
Ξ³ βΈ[ m α΅Β· p ] t β
Ξ΄ βΈ[ m ] u β
p Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ m ] prodβ p t u
prodβα΅£β +β€β§ βΈt βΈu = sub (prodββ βΈt βΈu) (+αΆβ€αΆβ§αΆ +β€β§)
prodα΅£ββ :
(β p q β p β§ q β€ p + q) β
Ξ³ βΈ[ m α΅Β· p ] t β
Ξ΄ βΈ[ m ] u β
p Β·αΆ Ξ³ β§αΆ Ξ΄ βΈ[ m ] prodα΅£ p t u
prodα΅£ββ β§β€+ βΈt βΈu = sub (prodα΅£β βΈt βΈu) (β§αΆβ€αΆ+αΆ β§β€+)
prodrecββ :
(m α΅Β· r Β· p PE.β‘ πα΅ β p β€ π) β
Ξ³ βΈ[ m α΅Β· r ] t β
Ξ΄ β β m β Β· r Β· p β β m β Β· r βΈ[ m ] u β
(β m β Β· r Β· (π + p)) Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ m ] prodrecβ p t u
prodrecββ {m = m} {r = r} {p = p} {Ξ³ = Ξ³} {Ξ΄ = Ξ΄} mrpβ‘πβpβ€π βΈt βΈu = sub
(doubleSubstβ-lemmaβ βΈu
(sndβ βΈt)
(fstβ (m α΅Β· r) (βΈ-cong (lemma m) (βΈ-Β· βΈt)) (α΅Β·-Β·-assoc m) mrpβ‘πβpβ€π))
(begin
(β m β Β· r Β· (π + p)) Β·αΆ Ξ³ +αΆ Ξ΄ ββ¨ +αΆ-comm _ _ β©
Ξ΄ +αΆ (β m β Β· r Β· (π + p)) Β·αΆ Ξ³ ββ¨ +αΆ-congΛ‘ $
βαΆ-trans
(Β·αΆ-congΚ³ $
PE.trans
(Β·-congΛ‘ $
PE.trans (Β·-distribΛ‘-+ _ _ _) $
+-congΚ³ $
Β·-identityΚ³ _) $
Β·-distribΛ‘-+ _ _ _) $
Β·αΆ-distribΚ³-+αΆ _ _ _ β©
Ξ΄ +αΆ (β m β Β· r) Β·αΆ Ξ³ +αΆ (β m β Β· r Β· p) Β·αΆ Ξ³ βΛβ¨ +αΆ-congΛ‘ $ +αΆ-congΛ‘ $
βαΆ-trans (βαΆ-sym (Β·αΆ-assoc _ _ _)) $
Β·αΆ-congΚ³ $
PE.trans (Β·-assoc _ _ _) $
Β·-congΛ‘ $
PE.trans (Β·-assoc _ _ _) $
Β·-congΛ‘ $
Β·ββββ β©
Ξ΄ +αΆ (β m β Β· r) Β·αΆ Ξ³ +αΆ (β m β Β· r Β· p) Β·αΆ β β p β β Β·αΆ Ξ³ β)
where
lemma : β m β β p β Β·α΅ m α΅Β· r PE.β‘ (m α΅Β· r) α΅Β· p
lemma πα΅ =
β p β Β·α΅ πα΅ β‘β¨ Β·α΅-zeroΚ³-πα΅ β©
πα΅ β
where
open Tools.Reasoning.PropositionalEquality
lemma πα΅ =
β p β Β·α΅ β r β β‘β¨ Β·α΅-comm β _ β _ β©
β r β Β·α΅ β p β β‘β¨ ββΒ·α΅ β©
β r Β· p β β‘Λβ¨ ββα΅Β· β©
β r β α΅Β· p β
where
open Tools.Reasoning.PropositionalEquality
open Tools.Reasoning.PartialOrder β€αΆ-poset
prodrecββ-πα΅ :
β¦ ok : T πα΅-allowed β¦ β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ β π β π βΈ[ πα΅ ] u β
Ξ΄ βΈ[ πα΅ ] prodrecβ p t u
prodrecββ-πα΅ {Ξ³ = Ξ³} {Ξ΄ = Ξ΄} {p = p} β¦ ok = ok β¦ βΈt βΈu = sub
(prodrecββ
(Ξ» ())
βΈt
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub βΈu $ begin
Ξ΄ β π Β· π Β· p β π Β· π ββ¨ βαΆ-refl β Β·-zeroΛ‘ _ β Β·-zeroΛ‘ _ β©
Ξ΄ β π β π β))
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ΄ βΛβ¨ +αΆ-identityΛ‘ _ β©
παΆ +αΆ Ξ΄ βΛβ¨ +αΆ-congΚ³ (Β·αΆ-zeroΛ‘ _) β©
π Β·αΆ Ξ³ +αΆ Ξ΄ βΛβ¨ +αΆ-congΚ³ (Β·αΆ-congΚ³ (Β·-zeroΛ‘ _)) β©
(π Β· π Β· (π + p)) Β·αΆ Ξ³ +αΆ Ξ΄ β)
prodrecββ-πα΅-π :
π β€ π β T πα΅-allowed β
Ξ³ βΈ[ β r β ] t β
Ξ΄ β π β r βΈ[ πα΅ ] u β
r Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ πα΅ ] prodrecβ π t u
prodrecββ-πα΅-π {Ξ³ = Ξ³} {r = r} {Ξ΄ = Ξ΄} ok βΈt βΈu = sub
(prodrecββ
(Ξ» βrπββ‘π β case ok of Ξ» where
(injβ πβ€π) β πβ€π
(injβ πα΅-ok) β let open Tools.Reasoning.PropositionalEquality in
case begin
πα΅[ πα΅-ok ] β‘Λβ¨ πα΅?β‘πα΅ β©
πα΅? β‘Λβ¨ βπββ‘πα΅? β©
β π β β‘Λβ¨ ββ-cong (Β·-zeroΚ³ r) β©
β r Β· π β β‘β¨ βrπββ‘π β©
πα΅ β
of Ξ» ())
βΈt
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub βΈu $ begin
Ξ΄ β π Β· r Β· π β π Β· r ββ¨ βαΆ-refl β PE.trans (Β·-congΛ‘ (Β·-zeroΚ³ _)) (Β·-zeroΚ³ _) β Β·-identityΛ‘ _ β©
Ξ΄ β π β r β))
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
r Β·αΆ Ξ³ +αΆ Ξ΄ βΛβ¨ +αΆ-congΚ³ $ Β·αΆ-congΚ³ $
PE.trans (Β·-identityΛ‘ _) $
PE.trans (Β·-congΛ‘ (+-identityΚ³ _)) $
Β·-identityΚ³ _ β©
(π Β· r Β· (π + π)) Β·αΆ Ξ³ +αΆ Ξ΄ β)
prodrecββ-πα΅-π :
Ξ³ βΈ[ β r β ] t β
Ξ΄ β r β r βΈ[ πα΅ ] u β
(r + r) Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ πα΅ ] prodrecβ π t u
prodrecββ-πα΅-π {Ξ³ = Ξ³} {r = r} {Ξ΄ = Ξ΄} βΈt βΈu = sub
(prodrecββ
(Ξ» _ β β€-refl)
βΈt
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub βΈu $ begin
Ξ΄ β π Β· r Β· π β π Β· r ββ¨ βαΆ-refl β PE.trans (Β·-identityΛ‘ _) (Β·-identityΚ³ _) β Β·-identityΛ‘ _ β©
Ξ΄ β r β r β))
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
(r + r) Β·αΆ Ξ³ +αΆ Ξ΄ βΛβ¨ +αΆ-congΚ³ $ Β·αΆ-congΚ³ $
PE.trans (Β·-identityΛ‘ _) $
PE.trans (Β·-distribΛ‘-+ _ _ _) $
+-cong (Β·-identityΚ³ _) (Β·-identityΚ³ _) β©
(π Β· r Β· (π + π)) Β·αΆ Ξ³ +αΆ Ξ΄ β)
prodrecββ-πα΅-π-β§β€+ :
(β p q β p β§ q β€ p + q) β
Ξ³ βΈ[ β r β ] t β
Ξ΄ β r β r βΈ[ πα΅ ] u β
r Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ πα΅ ] prodrecβ π t u
prodrecββ-πα΅-π-β§β€+ {Ξ³ = Ξ³} {r = r} {Ξ΄ = Ξ΄} β§β€+ βΈt βΈu = sub
(prodrecββ-πα΅-π βΈt βΈu)
(begin
r Β·αΆ Ξ³ +αΆ Ξ΄ βΛβ¨ +αΆ-congΚ³ (Β·αΆ-congΚ³ (β§-idem _)) β©
(r β§ r) Β·αΆ Ξ³ +αΆ Ξ΄ β€β¨ +αΆ-monotoneΛ‘ (Β·αΆ-monotoneΛ‘ (β§β€+ _ _)) β©
(r + r) Β·αΆ Ξ³ +αΆ Ξ΄ β)
where
open Tools.Reasoning.PartialOrder β€αΆ-poset
Β¬prodrecβ : Prodrec-allowed π π π
β Β¬ (π β€ π + π)
β Β¬ (β {n} {Ξ³ Ξ· : Conβ n} {Ξ΄ m r p q t u A}
β Ξ³ βΈ[ m α΅Β· r ] t
β Ξ΄ β β m β Β· r Β· p β β m β Β· r βΈ[ m ] u
β Ξ· β β πα΅? β Β· q βΈ[ πα΅? ] A
β Prodrec-allowed r p q
β r Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ m ] prodrecβ p t u)
Β¬prodrecβ ok πβ°π prodrecβββ² =
let t = prod Ξ£β π (var x0) (var x0)
u = prod Ξ£α΅£ π (var x1) (var x0)
Ξ³βΈtβ² = prodββ {Ξ³ = Ξ΅ β π} {m = πα΅} {p = π} {Ξ΄ = Ξ΅ β π}
(PE.subst (Ξ» x β _ βΈ[ x ] var x0) (PE.sym α΅Β·-identityΚ³) var)
(var {x = x0})
Ξ³βΈt = PE.substβ (Ξ» x y β x βΈ[ y ] t)
(PE.cong (Ξ΅ β_) (PE.trans (PE.cong (_β§ π) (Β·-identityΛ‘ π))
(β§-idem π)))
(PE.sym α΅Β·-identityΚ³) Ξ³βΈtβ²
Ξ΄βΈuβ² : _ βΈ[ πα΅ ] u
Ξ΄βΈuβ² = prodα΅£β var var
Ξ΄βΈu = let open Tools.Reasoning.PropositionalEquality
in PE.substβ (Ξ» x y z β Ξ΅ β x β y β z βΈ[ πα΅ ] u)
(PE.trans (+-identityΚ³ _) (Β·-identityΛ‘ π))
(π Β· β πα΅ α΅Β· π β + π β‘β¨ +-identityΚ³ _ β©
π Β· β πα΅ α΅Β· π β β‘β¨ Β·-identityΛ‘ _ β©
β πα΅ α΅Β· π β β‘β¨ PE.cong β_β (α΅Β·-identityΚ³ {m = πα΅}) β©
β πα΅ β β‘Λβ¨ Β·-identityΛ‘ _ β©
β πα΅ β Β· π β‘Λβ¨ Β·-identityΛ‘ _ β©
β πα΅ β Β· π Β· π β)
(π Β· π + β πα΅ β β‘β¨ PE.cong (_+ _) (Β·-identityΛ‘ π) β©
π + β πα΅ β β‘β¨ +-identityΛ‘ _ β©
β πα΅ β β‘Λβ¨ Β·-identityΚ³ _ β©
β πα΅ β Β· π β)
Ξ΄βΈuβ²
Ξ·βΈAβ² = Ξ Ξ£β {Ξ³ = παΆ} {p = π} {Ξ΄ = παΆ} {b = BMΞ£ Ξ£α΅£}
ββ (sub ββ (β€αΆ-refl β β€-reflexive (Β·-zeroΚ³ _)))
Ξ·βΈA = sub Ξ·βΈAβ² (β€αΆ-reflexive (βαΆ-sym (+αΆ-identityΛ‘ παΆ) β
PE.trans (Β·-zeroΚ³ _) (PE.sym (+-identityΛ‘ π))))
in case prodrecβββ² {Ξ· = παΆ} Ξ³βΈt Ξ΄βΈu Ξ·βΈA ok of Ξ» βΈprβ² β
case inv-usage-prodα΅£ βΈprβ² of Ξ» {
(invUsageProdα΅£ {Ξ΄ = Ξ΅ β a} {Ξ΅ β b} aβΈfstt bβΈsndt πβ€a+b) β case inv-usage-fst aβΈfstt of Ξ» {
(invUsageFst {Ξ΄ = Ξ΅ β c} mβ² eq cβΈt aβ€c _) β case inv-usage-snd bβΈsndt of Ξ» {
(invUsageSnd {Ξ΄ = Ξ΅ β d} dβΈt bβ€d) β case inv-usage-prodβ cβΈt of Ξ» {
(invUsageProdβ {Ξ΄ = Ξ΅ β e} {Ξ· = Ξ΅ β f} eβΈxβ fβΈxβ cβ€eβ§f) β case inv-usage-prodβ dβΈt of Ξ» {
(invUsageProdβ {Ξ΄ = Ξ΅ β g} {Ξ· = Ξ΅ β h} gβΈxβ hβΈxβ dβ€gβ§h) β
let i = β (πα΅ α΅Β· π) α΅Β· π β
j = β πα΅ α΅Β· π β
open Tools.Reasoning.PartialOrder β€-poset
in case begin
π β‘Λβ¨ Β·-identityΛ‘ π β©
π Β· π β‘Λβ¨ +-identityΚ³ _ β©
π Β· π + π β€β¨ β¦
πβ€a+b β¦ β©
π Β· a + b β‘β¨ PE.cong (_+ b) (Β·-identityΛ‘ a) β©
a + b β€β¨ +-monotone β¦
aβ€c β¦ β¦
bβ€d β¦ β©
c + d β€β¨ +-monotone β¦
cβ€eβ§f β¦ β¦
dβ€gβ§h β¦ β©
(π Β· e β§ f) + (π Β· g β§ h) β‘β¨ +-cong (β§-congΚ³ (Β·-identityΛ‘ e)) (β§-congΚ³ (Β·-identityΛ‘ g)) β©
(e β§ f) + (g β§ h) β€β¨ +-monotone (β§-monotone β¦
inv-usage-var eβΈxβ β¦ β¦
inv-usage-var fβΈxβ β¦)
(β§-monotone β¦
inv-usage-var gβΈxβ β¦ β¦
inv-usage-var hβΈxβ β¦)
β©
(i β§ j) + (j β§ π) β‘β¨ +-congΚ³ (β§-congΚ³ (PE.cong β_β ββΒ·α΅-idem)) β©
(j β§ j) + (j β§ π) β‘β¨ +-cong (β§-cong (PE.cong β_β βπβ) (PE.cong β_β βπβ))
(β§-congΚ³ (PE.cong β_β βπβ))
β©
(π β§ π) + (π β§ π) β‘β¨ +-cong (β§-idem π) (β§-idem π) β©
π + π β
of πβ°π
}}}}}
where
β¦
_β¦ : {p q : M} β Ξ΅ β p β€αΆ Ξ΅ β q β p β€ q
β¦
_β¦ = headβ-monotone
fstα΅£β² : M β M β M β Term n β Term n β Term n
fstα΅£β² r p q = Fstα΅£-sndα΅£.fstα΅£ r q p
inv-usage-fstα΅£β² :
Ξ³ βΈ[ m ] fstα΅£β² r p q A t β
ββ Ξ» Ξ· Ξ΄ β
Ξ³ β€αΆ r Β·αΆ Ξ· Γ
Ξ· βΈ[ m α΅Β· r ] t Γ
Ξ΄ βΈ[ πα΅? ] A Γ
β m β Β· r Β· p β€ β m β Γ
β m β Β· r β€ π Γ
Prodrec-allowed r p q
inv-usage-fstα΅£β² {Ξ³ = Ξ³} {m = m} {r = r} {p = p} {q = q} βΈfstα΅£β² =
case inv-usage-prodrec βΈfstα΅£β² of Ξ» {
(invUsageProdrec {Ξ΄ = Ξ΄} {Ξ· = Ξ·} {ΞΈ = ΞΈ} βΈt βΈvar βΈA ok Ξ³β€rΞ΄+Ξ·) β
case inv-usage-var βΈvar of Ξ» {
(Ξ·β€π β mrpβ€m β mrβ€π) β
Ξ΄
, ΞΈ
, (let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ³ β€β¨ Ξ³β€rΞ΄+Ξ· β©
r Β·αΆ Ξ΄ +αΆ Ξ· β€β¨ +αΆ-monotoneΚ³ Ξ·β€π β©
r Β·αΆ Ξ΄ +αΆ παΆ ββ¨ +αΆ-identityΚ³ _ β©
r Β·αΆ Ξ΄ β)
, βΈt
, wkUsageβ»ΒΉ βΈA
, mrpβ€m
, mrβ€π
, ok }}
inv-usage-fstα΅£β²-πα΅ :
Ξ³ βΈ[ πα΅ ] fstα΅£β² r p q A t β
ββ Ξ» Ξ· Ξ΄ β
Ξ³ β€αΆ r Β·αΆ Ξ· Γ
Ξ· βΈ[ β r β ] t Γ
Ξ΄ βΈ[ πα΅? ] A Γ
r Β· p β€ π Γ
r β€ π Γ
Prodrec-allowed r p q
inv-usage-fstα΅£β²-πα΅ {r = r} {p = p} βΈfstα΅£β² =
case inv-usage-fstα΅£β² βΈfstα΅£β² of Ξ» {
(_ , _ , leqβ , βΈt , βΈA , leqβ , leqβ , ok) β
_ , _ , leqβ , βΈt , βΈA ,
(begin
r Β· p β‘Λβ¨ Β·-identityΛ‘ _ β©
π Β· r Β· p β€β¨ leqβ β©
π β) ,
(begin
r β‘Λβ¨ Β·-identityΛ‘ _ β©
π Β· r β€β¨ leqβ β©
π β) ,
ok }
where
open Tools.Reasoning.PartialOrder β€-poset
πβ°πβfstα΅£β²-π-not-ok :
Β¬ π β€ π β
Β¬ Ξ³ βΈ[ πα΅ ] fstα΅£β² π p q A t
πβ°πβfstα΅£β²-π-not-ok {Ξ³ = Ξ³} {p = p} {q = q} {A = A} {t = t} πβ°π =
Ξ³ βΈ[ πα΅ ] fstα΅£β² π p q A t ββ¨ projβ ββ projβ ββ projβ ββ projβ ββ projβ ββ projβ ββ inv-usage-fstα΅£β²-πα΅ β©
π Β· p β€ π ββ¨ β€-trans (β€-reflexive (PE.sym (Β·-zeroΛ‘ _))) β©
π β€ π ββ¨ πβ°π β©
β₯ β‘
πβ°πβfstα΅£β²-π-not-ok :
Β¬ π β€ π β
Β¬ Ξ³ βΈ[ πα΅ ] fstα΅£β² π p q A t
πβ°πβfstα΅£β²-π-not-ok {Ξ³ = Ξ³} {p = p} {q = q} {A = A} {t = t} πβ°π =
Ξ³ βΈ[ πα΅ ] fstα΅£β² π p q A t ββ¨ projβ ββ projβ ββ projβ ββ projβ ββ projβ ββ projβ ββ projβ ββ inv-usage-fstα΅£β²-πα΅ β©
π β€ π ββ¨ πβ°π β©
β₯ β‘
inv-usage-fstα΅£β²-β’π-πα΅ :
r β’ π β π PE.β‘ π β
Ξ³ βΈ[ πα΅ ] fstα΅£β² r p q A t β
ββ Ξ» Ξ· Ξ΄ β
Ξ³ β€αΆ r Β·αΆ Ξ· Γ
Ξ· βΈ[ πα΅ ] t Γ
Ξ΄ βΈ[ πα΅? ] A Γ
r Β· p β€ π Γ
r β€ π Γ
Prodrec-allowed r p q
inv-usage-fstα΅£β²-β’π-πα΅ rβ’πβπβ‘π βΈfstα΅£β² =
case inv-usage-fstα΅£β²-πα΅ βΈfstα΅£β² of Ξ» {
(_ , _ , leqβ , βΈt , βΈA , leqβ , leqβ , ok) β
_ , _ , leqβ ,
βΈ-cong
(case rβ’πβπβ‘π of Ξ» where
(injβ rβ’π) β β’πββββ‘πα΅ rβ’π
(injβ πβ‘π) β Mode-propositional-if-πβ‘π πβ‘π)
βΈt ,
βΈA , leqβ , leqβ , ok }
inv-usage-fstα΅£β²-πβ§π-πα΅ :
Β¬ π β€ π β π PE.β‘ π β
Ξ³ βΈ[ πα΅ ] fstα΅£β² (π β§ π) p q A t β
ββ Ξ» Ξ· Ξ΄ β
Ξ³ β€αΆ παΆ β§αΆ Ξ· Γ Ξ· βΈ[ πα΅ ] t Γ
Ξ΄ βΈ[ πα΅? ] A Γ
π β§ p β€ π Γ
Prodrec-allowed (π β§ π) p q
inv-usage-fstα΅£β²-πβ§π-πα΅ {Ξ³ = Ξ³} {p = p} πβ°πβπβ‘π βΈfstα΅£β² =
case inv-usage-fstα΅£β²-β’π-πα΅ πβ§πβ’πβπβ‘π βΈfstα΅£β² of Ξ» {
(Ξ· , _ , leqβ , βΈt , βΈA , leqβ , _ , ok) β
_ , _ ,
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ³ β€β¨ leqβ β©
(π β§ π) Β·αΆ Ξ· β‘β¨ [πβ§π]Β·αΆβ‘παΆβ§αΆ β©
παΆ β§αΆ Ξ· β) ,
βΈt , βΈA ,
(let open Tools.Reasoning.PartialOrder β€-poset in begin
π β§ p β‘Λβ¨ [πβ§π]Β·β‘πβ§ β©
(π β§ π) Β· p β€β¨ leqβ β©
π β) ,
ok }
where
πβ§πβ’πβπβ‘π = case πβ°πβπβ‘π of Ξ» where
(injβ πβ°π) β injβ (πβ°πβπβ§πβ’π πβ°π)
(injβ πβ‘π) β injβ πβ‘π
fstα΅£β²βββ‘πβ€π :
{A : Term 1} β
(β {Ξ³ t} β
Ξ³ βΈ[ πα΅ ] t β
Ξ³ βΈ[ πα΅ ] fstα΅£β² r π q A t) β
r PE.β‘ π Γ π β€ π
fstα΅£β²βββ‘πβ€π {r = r} {q = q} {A = A} =
(β {Ξ³ t} β Ξ³ βΈ[ πα΅ ] t β Ξ³ βΈ[ πα΅ ] fstα΅£β² r π q A t) ββ¨ _$ var β©
Ξ³β² βΈ[ πα΅ ] fstα΅£β² r π q A tβ² ββ¨ lemma β©
r PE.β‘ π Γ π β€ π β‘
where
Ξ³β² = Ξ΅ β π
tβ² = var x0
lemma : Ξ³β² βΈ[ πα΅ ] fstα΅£β² r π q A tβ² β r PE.β‘ π Γ π β€ π
lemma βΈfst-t =
case inv-usage-fstα΅£β² βΈfst-t of Ξ» {
(Ξ΅ β p , _ , Ξ΅ β πβ€rp , βΈt , _ , πrπβ€π , πrβ€π , _) β
case inv-usage-var βΈt of Ξ» {
(Ξ΅ β pβ€ββrββ) β
let rβ€π = begin
r β‘Λβ¨ Β·-identityΚ³ _ β©
r Β· π β‘Λβ¨ Β·-identityΛ‘ _ β©
π Β· r Β· π β€β¨ πrπβ€π β©
π β
rβ€π = begin
r β‘Λβ¨ Β·-identityΛ‘ _ β©
π Β· r β€β¨ πrβ€π β©
π β
in
β€-antisym
rβ€π
(begin
π β€β¨ πβ€rp β©
r Β· p β€β¨ Β·-monotoneΚ³ pβ€ββrββ β©
r Β· β β r β β β‘β¨ Β·ββββ β©
r β)
, (begin
π β€β¨ πβ€rp β©
r Β· p β€β¨ Β·-monotoneΛ‘ rβ€π β©
π Β· p β‘β¨ Β·-zeroΛ‘ _ β©
π β) }}
where
open Tools.Reasoning.PartialOrder β€-poset
Β¬fstα΅£β²ββ² :
{A : Term 1} β
Β¬ π β€ π β
Β¬ ({Ξ³ : Conβ 1} {t : Term 1} β
Ξ³ βΈ[ πα΅ ] t β
Ξ³ βΈ[ πα΅ ] fstα΅£β² r π q A t)
Β¬fstα΅£β²ββ² πβ°π hyp = πβ°π (fstα΅£β²βββ‘πβ€π hyp .projβ)
Β¬fstα΅£β²β :
Β¬ π β€ π β
Β¬ (β {Ξ³ : Conβ 1} {t : Term 1} {p mβ²} m β
Ξ³ βΈ[ m α΅Β· p ] t β
m α΅Β· p PE.β‘ mβ² β
(mβ² PE.β‘ πα΅ β p β€ π) β
Ξ³ βΈ[ mβ² ] fstα΅£β² r p q A t)
Β¬fstα΅£β²β πβ°π hyp =
Β¬fstα΅£β²ββ² πβ°π Ξ» βΈt β
hyp πα΅ (βΈ-cong (PE.sym βπβ) βΈt) βπβ (Ξ» _ β β€-refl)
open Fstα΅£-sndα΅£ (π β§ π) π public using (fstα΅£; sndα΅£)
inv-usage-fstα΅£ :
Β¬ π β€ π β π PE.β‘ π β m β’ πα΅ β
Ξ³ βΈ[ m ] fstα΅£ p A t β
ββ Ξ» Ξ· Ξ΄ β
Ξ³ β€αΆ παΆ β§αΆ Ξ· Γ Ξ· βΈ[ m ] t Γ
Ξ΄ βΈ[ πα΅? ] A Γ
π β§ β m β Β· p β€ β m β Γ
Prodrec-allowed (π β§ π) p π
inv-usage-fstα΅£ {m = m} {Ξ³ = Ξ³} {p = p} πβ°πβπβ‘πββ’πα΅ βΈfstα΅£ =
case inv-usage-fstα΅£β² βΈfstα΅£ of Ξ» {
(Ξ· , Ξ΄ , leqβ , βΈt , βΈA , leqβ , leqβ , ok) β
_ , _ ,
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ³ β€β¨ leqβ β©
(π β§ π) Β·αΆ Ξ· β‘β¨ [πβ§π]Β·αΆβ‘παΆβ§αΆ β©
παΆ β§αΆ Ξ· β) ,
βΈ-cong (πβ°πβπβ‘πββ’πα΅βα΅Β·[πβ§π]β‘ _ πβ°πβπβ‘πββ’πα΅) βΈt ,
βΈA ,
(let open Tools.Reasoning.PartialOrder β€-poset in begin
π β§ β m β Β· p β‘Λβ¨ Β·[πβ§π]Β·β‘πβ§Β· β©
β m β Β· (π β§ π) Β· p β€β¨ leqβ β©
β m β β) ,
ok }
inv-usage-fstα΅£-πα΅ :
β¦ ok : T πα΅-allowed β¦ β
Ξ³ βΈ[ πα΅ ] fstα΅£ p A t β
β Ξ» Ξ΄ β
Ξ³ β€αΆ παΆ Γ παΆ βΈ[ πα΅ ] t Γ
Ξ΄ βΈ[ πα΅ ] A Γ
Prodrec-allowed (π β§ π) p π
inv-usage-fstα΅£-πα΅ {Ξ³ = Ξ³} βΈfstα΅£ =
case inv-usage-fstα΅£ (injβ (injβ (Ξ» ()))) βΈfstα΅£ of Ξ» {
(Ξ· , _ , leqβ , βΈt , βΈA , leqβ , ok) β
_ ,
(begin
Ξ³ β€β¨ leqβ β©
παΆ β§αΆ Ξ· β€β¨ β§αΆ-decreasingΚ³ _ _ β©
Ξ· β€β¨ βΈ-πα΅ βΈt β©
παΆ β) ,
(sub (βΈ-Β· {mβ² = πα΅} βΈt) $ begin
παΆ βΛβ¨ Β·αΆ-zeroΛ‘ _ β©
π Β·αΆ Ξ· β) ,
βΈ-cong πα΅?β‘πα΅ βΈA , ok }
where
open Tools.Reasoning.PartialOrder β€αΆ-poset
inv-usage-fstα΅£-πα΅ :
Β¬ π β€ π β π PE.β‘ π β
Ξ³ βΈ[ πα΅ ] fstα΅£ p A t β
ββ Ξ» Ξ· Ξ΄ β
Ξ³ β€αΆ παΆ β§αΆ Ξ· Γ Ξ· βΈ[ πα΅ ] t Γ
Ξ΄ βΈ[ πα΅? ] A Γ
π β§ p β€ π Γ
Prodrec-allowed (π β§ π) p π
inv-usage-fstα΅£-πα΅ {p = p} πβ°πβπβ‘π βΈfstα΅£ =
case inv-usage-fstα΅£ πβ°πβπβ‘πβπα΅β’πα΅ βΈfstα΅£ of Ξ» {
(_ , _ , leqβ , βΈt , βΈA , leqβ , ok) β
_ , _ , leqβ , βΈt , βΈA ,
(begin
π β§ p β‘Λβ¨ β§-congΛ‘ (Β·-identityΛ‘ _) β©
π β§ π Β· p β€β¨ leqβ β©
π β) ,
ok }
where
open Tools.Reasoning.PartialOrder β€-poset
πβ°πβπβ‘πβπα΅β’πα΅ = case πβ°πβπβ‘π of Ξ» where
(injβ πβ°π) β injβ πβ°π
(injβ πβ‘π) β injβ (injβ πβ‘π)
fstα΅£β :
Β¬ π β€ π β π PE.β‘ π β m β’ πα΅ β
π β§ β m β Β· p β€ β m β β
Prodrec-allowed (π β§ π) p π β
Ξ³ βΈ[ m ] t β
Ξ΄ βΈ[ πα΅? ] A β
παΆ β§αΆ Ξ³ βΈ[ m ] fstα΅£ p A t
fstα΅£β {m = m} {p = p} {Ξ³ = Ξ³} {Ξ΄ = Ξ΄} πβ°πβπβ‘πββ’πα΅ πβ§mpβ€m ok βΈt βΈA = sub
(prodrecβ
(βΈ-cong (PE.sym (πβ°πβπβ‘πββ’πα΅βα΅Β·[πβ§π]β‘ _ πβ°πβπβ‘πββ’πα΅)) βΈt)
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub var $ begin
παΆ β β m β Β· (π β§ π) Β· p β β m β Β· (π β§ π) ββ¨ βαΆ-refl β Β·[πβ§π]Β·β‘πβ§Β· β Β·[πβ§π]β‘πβ§ β©
παΆ β π β§ β m β Β· p β π β§ β m β β€β¨ β€αΆ-refl β πβ§mpβ€m β β§-decreasingΛ‘ _ _ β©
παΆ β β m β β π β)
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub (wkUsage (step id) βΈA) $ begin
Ξ΄ β β πα΅? β Β· π ββ¨ βαΆ-refl β Β·-zeroΚ³ _ β©
Ξ΄ β π β)
ok)
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
παΆ β§αΆ Ξ³ β‘Λβ¨ [πβ§π]Β·αΆβ‘παΆβ§αΆ β©
(π β§ π) Β·αΆ Ξ³ βΛβ¨ +αΆ-identityΚ³ _ β©
(π β§ π) Β·αΆ Ξ³ +αΆ παΆ β)
fstα΅£β-πα΅ :
β¦ ok : T πα΅-allowed β¦ β
Prodrec-allowed (π β§ π) p π β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ βΈ[ πα΅ ] A β
Ξ³ βΈ[ πα΅ ] fstα΅£ p A t
fstα΅£β-πα΅ {p = p} {Ξ³ = Ξ³} {Ξ΄ = Ξ΄} ok βΈt βΈA = sub
(fstα΅£β
(injβ (injβ (Ξ» ())))
(let open Tools.Reasoning.PartialOrder β€-poset in begin
π β§ π Β· p β‘β¨ β§-congΛ‘ (Β·-zeroΛ‘ _) β©
π β§ π β‘β¨ β§-idem _ β©
π β)
ok
βΈt
(βΈ-cong (PE.sym πα΅?β‘πα΅) βΈA))
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ³ β€β¨ β§αΆ-greatest-lower-bound (βΈ-πα΅ βΈt) β€αΆ-refl β©
παΆ β§αΆ Ξ³ β)
fstα΅£β-πα΅ :
Β¬ π β€ π β π PE.β‘ π β
π β§ p β€ π β
Prodrec-allowed (π β§ π) p π β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ βΈ[ πα΅? ] A β
παΆ β§αΆ Ξ³ βΈ[ πα΅ ] fstα΅£ p A t
fstα΅£β-πα΅ {p = p} πβ°πβπβ’π πβ§pβ€π = fstα΅£β
(case πβ°πβπβ’π of Ξ» where
(injβ πβ°π) β injβ πβ°π
(injβ πβ’π) β injβ (injβ πβ’π))
(begin
π β§ π Β· p β‘β¨ β§-congΛ‘ (Β·-identityΛ‘ _) β©
π β§ p β€β¨ πβ§pβ€π β©
π β)
where
open Tools.Reasoning.PartialOrder β€-poset
fstα΅£β-πα΅-β€π :
π PE.β‘ π β π β’ π β
(β p β p β€ π) β
p β€ π β
Prodrec-allowed (π β§ π) p π β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ βΈ[ πα΅? ] A β
Ξ³ βΈ[ πα΅ ] fstα΅£ p A t
fstα΅£β-πα΅-β€π {p = p} {Ξ³ = Ξ³} πβ‘πβπβ’π β€π pβ€π ok βΈt βΈA = sub
(fstα΅£β-πα΅
(β€πβπβ°πβπβ‘π πβ‘πβπβ’π β€π)
(let open Tools.Reasoning.PartialOrder β€-poset in begin
π β§ p β€β¨ β§-decreasingΚ³ _ _ β©
p β€β¨ pβ€π β©
π β)
ok
βΈt
βΈA)
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ³ β€β¨ β§αΆ-greatest-lower-bound (β€αΆπαΆ (β€π _)) β€αΆ-refl β©
παΆ β§αΆ Ξ³ β)
fstα΅£β-πα΅-β§β€+ :
π PE.β‘ π β π β’ π β
(β p q β p + q β€ p β§ q) β
p β€ π β
Prodrec-allowed (π β§ π) p π β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ βΈ[ πα΅? ] A β
Ξ³ βΈ[ πα΅ ] fstα΅£ p A t
fstα΅£β-πα΅-β§β€+ πβ‘πβπβ’π +β€β§ = fstα΅£β-πα΅-β€π πβ‘πβπβ’π (+β€β§ββ€π +β€β§)
Β¬fstα΅£ββ² :
{A : Term 1} β
Β¬ π β€ π β
Β¬ ({Ξ³ : Conβ 1} {t : Term 1} β
Ξ³ βΈ[ πα΅ ] t β
Ξ³ βΈ[ πα΅ ] fstα΅£ π A t)
Β¬fstα΅£ββ² = Β¬fstα΅£β²ββ²
Β¬fstα΅£β :
Β¬ π β€ π β
Β¬ (β {Ξ³ : Conβ 1} {t : Term 1} {p mβ²} m β
Ξ³ βΈ[ m α΅Β· p ] t β
m α΅Β· p PE.β‘ mβ² β
(mβ² PE.β‘ πα΅ β p β€ π) β
Ξ³ βΈ[ mβ² ] fstα΅£ p A t)
Β¬fstα΅£β = Β¬fstα΅£β²β
inv-usage-sndα΅£ :
Β¬ π β€ π β π PE.β‘ π β m β’ πα΅ β
β B β
Ξ³ βΈ[ m ] sndα΅£ p q A B t β
ββ Ξ» Ξ· Ξ΄ β
Ξ³ β€αΆ παΆ β§αΆ Ξ· Γ Ξ· βΈ[ m ] t Γ
Ξ΄ β β πα΅? β Β· q βΈ[ πα΅? ] B [ fstα΅£ p (wk1 A) (var x0) ]β Γ
Prodrec-allowed (π β§ π) p q
inv-usage-sndα΅£ {Ξ³ = Ξ³} πβ°πβπβ‘πββ’πα΅ _ βΈsndα΅£ =
case inv-usage-prodrec βΈsndα΅£ of Ξ» {
(invUsageProdrec {Ξ΄ = Ξ΄} {Ξ· = Ξ·} {ΞΈ = ΞΈ} βΈt βΈvar βΈB ok Ξ³β€[πβ§π]Ξ΄+Ξ·) β
case inv-usage-var βΈvar of Ξ» {
(Ξ·β€π β _ β _) β
Ξ΄
, ΞΈ
, (begin
Ξ³ β€β¨ Ξ³β€[πβ§π]Ξ΄+Ξ· β©
(π β§ π) Β·αΆ Ξ΄ +αΆ Ξ· β€β¨ +αΆ-monotoneΚ³ Ξ·β€π β©
(π β§ π) Β·αΆ Ξ΄ +αΆ παΆ ββ¨ +αΆ-identityΚ³ _ β©
(π β§ π) Β·αΆ Ξ΄ β‘β¨ [πβ§π]Β·αΆβ‘παΆβ§αΆ β©
παΆ β§αΆ Ξ΄ β)
, βΈ-cong (πβ°πβπβ‘πββ’πα΅βα΅Β·[πβ§π]β‘ _ πβ°πβπβ‘πββ’πα΅) βΈt
, βΈB
, ok }}
where
open Tools.Reasoning.PartialOrder β€αΆ-poset
inv-usage-sndα΅£-πα΅ :
β¦ ok : T πα΅-allowed β¦ β
β B β
Ξ³ βΈ[ πα΅ ] sndα΅£ p q A B t β
β Ξ» Ξ΄ β
Ξ³ β€αΆ παΆ Γ παΆ βΈ[ πα΅ ] t Γ
Ξ΄ β π βΈ[ πα΅ ] B [ fstα΅£ p (wk1 A) (var x0) ]β Γ
Prodrec-allowed (π β§ π) p q
inv-usage-sndα΅£-πα΅ {Ξ³ = Ξ³} {q = q} β¦ ok = πα΅-ok β¦ B βΈsndα΅£ =
case inv-usage-sndα΅£ (injβ (injβ (Ξ» ()))) B βΈsndα΅£ of Ξ» {
(Ξ· , Ξ΄ , leq , βΈt , βΈB , ok) β
_
, (let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ³ β€β¨ leq β©
παΆ β§αΆ Ξ· β€β¨ β§αΆ-decreasingΚ³ _ _ β©
Ξ· β€β¨ βΈ-πα΅ βΈt β©
παΆ β)
, (let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub (βΈ-Β· {mβ² = πα΅} βΈt) $ begin
παΆ βΛβ¨ Β·αΆ-zeroΛ‘ _ β©
π Β·αΆ Ξ· β)
, (let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub (βΈ-cong πα΅?β‘πα΅ βΈB) $ begin
Ξ΄ β π βΛβ¨ βαΆ-refl β Β·-zeroΛ‘ _ β©
Ξ΄ β π Β· q βΛβ¨ βαΆ-refl β Β·-congΚ³ (PE.cong β_β (πα΅?β‘πα΅ {ok = πα΅-ok})) β©
Ξ΄ β β πα΅? β Β· q β)
, ok }
sndα΅£β :
Β¬ π β€ π β π PE.β‘ π β m β’ πα΅ β
Prodrec-allowed (π β§ π) p q β
β B β
Ξ³ βΈ[ m ] t β
Ξ΄ β β πα΅? β Β· q βΈ[ πα΅? ] B [ fstα΅£ p (wk1 A) (var x0) ]β β
παΆ β§αΆ Ξ³ βΈ[ m ] sndα΅£ p q A B t
sndα΅£β {m = m} {p = p} {Ξ³ = Ξ³} πβ°πβπβ‘πββ’πα΅ ok _ βΈt βΈB = sub
(prodrecβ
(βΈ-cong (PE.sym (πβ°πβπβ‘πββ’πα΅βα΅Β·[πβ§π]β‘ _ πβ°πβπβ‘πββ’πα΅)) βΈt)
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub var $ begin
παΆ β β m β Β· (π β§ π) Β· p β β m β Β· (π β§ π) ββ¨ βαΆ-refl β Β·[πβ§π]Β·β‘πβ§Β· β Β·[πβ§π]β‘πβ§ β©
παΆ β π β§ β m β Β· p β π β§ β m β β€β¨ β€αΆ-refl β β§-decreasingΛ‘ _ _ β β§-decreasingΚ³ _ _ β©
παΆ β π β β m β β)
βΈB
ok)
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
παΆ β§αΆ Ξ³ β‘Λβ¨ [πβ§π]Β·αΆβ‘παΆβ§αΆ β©
(π β§ π) Β·αΆ Ξ³ βΛβ¨ +αΆ-identityΚ³ _ β©
(π β§ π) Β·αΆ Ξ³ +αΆ παΆ β)
sndα΅£β-πα΅ :
β¦ ok : T πα΅-allowed β¦ β
Prodrec-allowed (π β§ π) p q β
β B β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ β π βΈ[ πα΅ ] B [ fstα΅£ p (wk1 A) (var x0) ]β β
Ξ³ βΈ[ πα΅ ] sndα΅£ p q A B t
sndα΅£β-πα΅ {p = p} {q = q} {Ξ³ = Ξ³} {Ξ΄ = Ξ΄} β¦ ok = πα΅-ok β¦ ok B βΈt βΈB = sub
(sndα΅£β
(injβ (injβ (Ξ» ())))
ok
B
βΈt
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in
sub (βΈ-cong (PE.sym πα΅?β‘πα΅) βΈB) $ begin
Ξ΄ β β πα΅? β Β· q ββ¨ βαΆ-refl β Β·-congΚ³ (PE.cong β_β (πα΅?β‘πα΅ {ok = πα΅-ok})) β©
Ξ΄ β π Β· q ββ¨ βαΆ-refl β Β·-zeroΛ‘ _ β©
Ξ΄ β π β))
(let open Tools.Reasoning.PartialOrder β€αΆ-poset in begin
Ξ³ β€β¨ β§αΆ-greatest-lower-bound (βΈ-πα΅ βΈt) β€αΆ-refl β©
παΆ β§αΆ Ξ³ β)
sndα΅£β-πα΅-β€π :
π PE.β‘ π β π β’ π β
(β p β p β€ π) β
Prodrec-allowed (π β§ π) p q β
β B β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ β β πα΅? β Β· q βΈ[ πα΅? ] B [ fstα΅£ p (wk1 A) (var x0) ]β β
Ξ³ βΈ[ πα΅ ] sndα΅£ p q A B t
sndα΅£β-πα΅-β€π {Ξ³ = Ξ³} πβ‘πβπβ’π β€π ok B βΈt βΈB = sub
(sndα΅£β
(case β€πβπβ°πβπβ‘π πβ‘πβπβ’π β€π of Ξ» where
(injβ πβ°π) β injβ πβ°π
(injβ πβ‘π) β injβ (injβ πβ‘π))
ok
B
βΈt
βΈB)
(begin
Ξ³ β€β¨ β§αΆ-greatest-lower-bound (β€αΆπαΆ (β€π _)) β€αΆ-refl β©
παΆ β§αΆ Ξ³ β)
where
open Tools.Reasoning.PartialOrder β€αΆ-poset
sndα΅£β-πα΅-+β€β§ :
π PE.β‘ π β π β’ π β
(β p q β p + q β€ p β§ q) β
Prodrec-allowed (π β§ π) p q β
β B β
Ξ³ βΈ[ πα΅ ] t β
Ξ΄ β β πα΅? β Β· q βΈ[ πα΅? ] B [ fstα΅£ p (wk1 A) (var x0) ]β β
Ξ³ βΈ[ πα΅ ] sndα΅£ p q A B t
sndα΅£β-πα΅-+β€β§ πβ‘πβπβ’π +β€β§ = sndα΅£β-πα΅-β€π πβ‘πβπβ’π (+β€β§ββ€π +β€β§)
sndα΅£ββπβ€π :
{A : Term 1} (B : Term 2) β
(β {Ξ³ t} β
Ξ³ βΈ[ πα΅ ] t β
Ξ³ βΈ[ πα΅ ] sndα΅£ p q A B t) β
π β€ π
sndα΅£ββπβ€π {p = p} {q = q} {A = A} B =
(β {Ξ³ t} β Ξ³ βΈ[ πα΅ ] t β Ξ³ βΈ[ πα΅ ] sndα΅£ p q A B t) ββ¨ _$ var β©
Ξ³β² βΈ[ πα΅ ] sndα΅£ p q A B tβ² ββ¨ lemma β©
π β€ π β‘
where
Ξ³β² = Ξ΅ β π
tβ² = var x0
lemma : Ξ³β² βΈ[ πα΅ ] sndα΅£ p q A B tβ² β π β€ π
lemma βΈsnd-t =
case inv-usage-prodrec βΈsnd-t of Ξ» {
(invUsageProdrec
{Ξ΄ = Ξ΅ β r} {Ξ· = Ξ΅ β s} βΈt βΈvar _ _ (Ξ΅ β πβ€[πβ§π]r+s)) β
case inv-usage-var βΈvar of Ξ» {
(Ξ΅ β sβ€π β _ β _) β
case inv-usage-var βΈt of Ξ» {
(Ξ΅ β rβ€ββπβ§πββ) β
begin
π β€β¨ πβ€[πβ§π]r+s β©
(π β§ π) Β· r + s β€β¨ +-monotoneΚ³ sβ€π β©
(π β§ π) Β· r + π β‘β¨ +-identityΚ³ _ β©
(π β§ π) Β· r β€β¨ Β·-monotoneΚ³ rβ€ββπβ§πββ β©
(π β§ π) Β· β β π β§ π β β β‘β¨ Β·ββββ β©
π β§ π β€β¨ β§-decreasingΛ‘ _ _ β©
π β }}}
where
open Tools.Reasoning.PartialOrder β€-poset
Β¬sndα΅£β :
{A : Term 1} (B : Term 2) β
Β¬ π β€ π β
Β¬ ({Ξ³ : Conβ 1} {t : Term 1} β
Ξ³ βΈ[ πα΅ ] t β
Ξ³ βΈ[ πα΅ ] sndα΅£ p q A B t)
Β¬sndα΅£β B πβ°π hyp = πβ°π (sndα΅£ββπβ€π B hyp)