Partial/MutualNestedCalls

Partial/DomEven.agda

@@ -19,6 +19,37 @@ module f-bad where
   f (suc zero) = ω
   f (suc (suc n)) = suc (suc (f n))
 
+  -- No calls to `f` are unfolded. Hence, `f 2` won't reduce to 2.
+
+  f2≡f2 : f 2 ≡ f 2
+  f2≡f2 = refl
+
+  -- The following theorem is "true", in a sense.
+  -- But what is the sense? :-)
+
+  f1≡f1 : f 1 ≡ f 1
+  f1≡f1 = refl
+
+module f-bad2 where
+
+  {-# TERMINATING #-}
+  f : ℕ → ℕ
+  f zero = zero
+  f (suc zero) = ω
+  f (suc (suc n)) = suc (suc (f n))
+
+  -- Now calls to `f` are unfolded. Hence, `f 2` reduces to 2.
+
+  f2≡f2 : f 2 ≡ 2
+  f2≡f2 = refl
+
+  -- However, if we try to normalize f 1, the Agda compiler will go
+  -- into an infinite loop!
+  -- Because we make Agda belive that the function is total, while it is not!
+
+  -- f1≡f1 : f 1 ≡ f 1
+  -- f1≡f1 = refl
+
 module f-good where
 
   -- Now we specify the domain of `f` following Bove & Capretta's technique.
@@ -28,27 +59,27 @@ module f-good where
   -- is required.
 
   data F : ℕ → Set where
-    d0 : F zero
-    d2 : ∀ {n} → F n → F (suc (suc n))
+    a0 : F zero
+    a2 : ∀ {n} (fn⇓ : F n) → F (suc (suc n))
 
-  f : (n : ℕ) (h : F n) → ℕ
-  f zero d0 = zero
+  f : (n : ℕ) (fn⇓ : F n) → ℕ
+  f zero a0 = zero
   f (suc zero) ()
-  f (suc (suc n)) (d2 h) = suc (suc (f n h))
+  f (suc (suc n)) (a2 fn⇓) = suc (suc (f n fn⇓))
 
-  hf4 : F 4
-  hf4 = d2 (d2 d0)
+  f4⇓ : F 4
+  f4⇓ = a2 (a2 a0)
 
-  f4≡4 : f 4 hf4 ≡ 4
+  f4≡4 : f 4 f4⇓ ≡ 4
   f4≡4 = refl
 
   -- We can prove theorems about partial functions.
 
-  f-id : (n : ℕ) (h : F n) → f n h ≡ n
-  f-id zero d0 = refl
-  f-id (suc zero) ()
-  f-id (suc (suc n)) (d2 h) =
-    cong (suc ∘ suc) (f-id n h)
+  fn≡n : (n : ℕ) (fn⇓ : F n) → f n fn⇓ ≡ n
+  fn≡n zero a0 = refl
+  fn≡n (suc zero) ()
+  fn≡n (suc (suc n)) (a2 fn⇓) =
+    cong (suc ∘ suc) (fn≡n n fn⇓)
 
 module fg-bad where
 
@@ -72,34 +103,34 @@ module fg-good where
   mutual
 
     data F : ℕ → Set where
-      f0 : F zero
-      f1 : ∀ {n} (h : G n) → F (suc n)
+      a0 : F zero
+      a1 : ∀ {n} (gn⇓ : G n) → F (suc n)
 
     data G : ℕ → Set where
-      g1 : ∀ {n} (h : F n) → G (suc n)
+      b1 : ∀ {n} (fn⇓ : F n) → G (suc n)
 
   mutual
 
-    f : (n : ℕ) (h : F n) → ℕ
-    f zero f0 = zero
-    f (suc n) (f1 h) = suc (g n h)
+    f : (n : ℕ) (fn⇓ : F n) → ℕ
+    f zero a0 = zero
+    f (suc n) (a1 gn⇓) = suc (g n gn⇓)
 
-    g : (n : ℕ) (h : G n) → ℕ
+    g : (n : ℕ) (gn⇓ : G n) → ℕ
     g zero ()
-    g (suc n) (g1 h) = suc (f n h)
+    g (suc n) (b1 fn⇓) = suc (f n fn⇓)
 
-    hf4 : F 4
-    hf4 = f1 (g1 (f1 (g1 f0)))
+    f4⇓ : F 4
+    f4⇓ = a1 (b1 (a1 (b1 a0)))
 
-    f4≡4 : f 4 hf4 ≡ 4
+    f4≡4 : f 4 f4⇓ ≡ 4
     f4≡4 = refl
 
   mutual
 
-    f-id : (n : ℕ) (h : F n) → f n h ≡ n
-    f-id zero f0 = refl
-    f-id (suc n) (f1 h) = cong suc (g-id n h)
+    fn≡n : (n : ℕ) (fn⇓ : F n) → f n fn⇓ ≡ n
+    fn≡n zero a0 = refl
+    fn≡n (suc n) (a1 gn⇓) = cong suc (gn≡n n gn⇓)
 
-    g-id : (n : ℕ) (h : G n) → g n h ≡ n
-    g-id zero ()
-    g-id (suc n) (g1 h) = cong suc (f-id n h)
+    gn≡n : (n : ℕ) (gn⇓ : G n) → g n gn⇓ ≡ n
+    gn≡n zero ()
+    gn≡n (suc n) (b1 fn⇓) = cong suc (fn≡n n fn⇓)

Partial/Find.agda

@@ -62,32 +62,32 @@ module Find-good where
     mutual
 
       data Find : ℕ → Set where
-        f0 : ∀ {n} → Find′ n (p n) → Find n
+        a0 : ∀ {n} → Find′ n (p n) → Find n
 
       data Find′ : ℕ → Bool → Set where
-        g0 : ∀ {n} → Find′ n true
-        g1 : ∀ {n} → Find (suc n) → Find′ n false
+        b0 : ∀ {n} → Find′ n true
+        b1 : ∀ {n} → Find (suc n) → Find′ n false
 
     mutual
 
       find : (n : ℕ) (h : Find n) → ℕ
-      find n (f0 h) = find′ n (p n) h
+      find n (a0 h) = find′ n (p n) h
 
       find′ : (n : ℕ) (b : Bool) (h : Find′ n b) → ℕ
-      find′ n true g0 = n
-      find′ n false (g1 h) = find (suc n) h
+      find′ n true b0 = n
+      find′ n false (b1 h) = find (suc n) h
 
   ge3! : Find ge3 0
-  ge3! = f0 (g1 (f0 (g1 (f0 (g1 (f0 g0))))))
+  ge3! = a0 (b1 (a0 (b1 (a0 (b1 (a0 b0))))))
 
   find-ge3≡3 : ℕ
   find-ge3≡3 = find ge3 0 ge3!
 
   correct : ∀ p n → (h : Find p n) → p (find p n h) ≡ true
-  correct p n (f0 h) with p n | inspect p n
-  correct p n (f0 g0) | true | [ pn≡true ] =
+  correct p n (a0 h) with p n | inspect p n
+  correct p n (a0 b0) | true | [ pn≡true ] =
     pn≡true
-  correct p n (f0 (g1 h)) | false | [ pn≡false ] =
+  correct p n (a0 (b1 h)) | false | [ pn≡false ] =
     correct p (suc n) h
 
 module Find-dec-bad where
@@ -136,24 +136,22 @@ module Find-dec-good where
 
     mutual
 
-      data Find : (n : ℕ) → Set
-        where
-        f0 : ∀ {n} → Find′ n (p? n) → Find n
+      data Find : (n : ℕ) → Set where
+        a0 : ∀ {n} → Find′ n (p? n) → Find n
 
-      data Find′ : (n : ℕ) (pn : Dec (P n)) → Set
-        where
-        g0 : ∀ {n pn} → Find′ n (yes pn)
-        g1 : ∀ {n ¬pn} → Find (suc n) → Find′ n (no ¬pn)
+      data Find′ : (n : ℕ) (pn : Dec (P n)) → Set where
+        b0 : ∀ {n pn} → Find′ n (yes pn)
+        b1 : ∀ {n ¬pn} → Find (suc n) → Find′ n (no ¬pn)
 
       find : (n : ℕ) (h : Find n) → ∃ λ m → P m
-      find n (f0 h) = find′ n (p? n) h
+      find n (a0 h) = find′ n (p? n) h
 
       find′ : (n : ℕ) (pn : Dec (P n)) (h : Find′ n pn) → (∃ λ m → P m)
-      find′ n (yes pn) g0 = n , pn
-      find′ n (no ¬pn) (g1 h) = find (suc n) h
+      find′ n (yes pn) b0 = n , pn
+      find′ n (no ¬pn) (b1 h) = find (suc n) h
 
   ge3! : Find ge3? 0
-  ge3! = f0 (g1 (f0 (g1 (f0 (g1 (f0 g0))))))
+  ge3! = a0 (b1 (a0 (b1 (a0 (b1 (a0 b0))))))
 
   find-ge3?≡ : find ge3? 0 ge3! ≡ (3 , s≤s (s≤s (s≤s z≤n)))
   find-ge3?≡ = refl

Partial/MutualNestedCalls.agda

@@ -0,0 +1,137 @@
+module Partial.MutualNestedCalls where
+
+open import Data.Nat
+
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+module fg-bad where
+
+  -- Here the functions `f` and `g` are total, but Agda is unable to prove it.
+  -- So we just postulate the totality by means of a pragma.
+
+  mutual
+
+    {-# TERMINATING #-}
+
+    f : ℕ → ℕ
+    f zero = zero
+    f (suc n) = suc (f (g n))
+
+    g : ℕ → ℕ
+    g zero = zero
+    g (suc n) = suc (g (f n))
+
+    f5≡0 : f 5 ≡ 5
+    f5≡0 = refl
+
+  -- This proof is not completely formal, since it uses the totality of `f` that
+  -- has been just postulated.
+
+  mutual
+
+    fn≡n : ∀ n → f n ≡ n
+    fn≡n zero = refl
+    fn≡n (suc n) = cong suc (
+      f (g n)
+        ≡⟨ cong f (gn≡n n) ⟩
+      f n
+        ≡⟨ fn≡n n ⟩
+      n ∎)
+
+    gn≡n : ∀ n → g n ≡ n
+    gn≡n zero = refl
+    gn≡n (suc n) rewrite fn≡n n | gn≡n n =
+      refl
+
+mutual
+
+  -- Now we specify the domains of `f` and `g` by using
+  -- Bove & Capretta's technique.
+  -- Note that we have to define `F`, `G`, `f` and `g` simultaneously,
+  -- because the definitions of `f` and `g` contain nested function calls.
+
+  data F : (n : ℕ) → Set where
+    a0 : F zero
+    a1 : ∀ {n} (gn⇓ : G n) (fgn⇓ : F (g n gn⇓)) → F (suc n)
+
+  f : (n : ℕ) → F n → ℕ
+  f zero a0 = zero
+  f (suc n) (a1 gn⇓ fgn⇓) = suc (f (g n gn⇓) fgn⇓)
+
+  data G : (n : ℕ) → Set where
+    b0 : G zero
+    b1 : ∀ {n} (fn⇓ : F n) (gfn⇓ : G (f n fn⇓)) → G (suc n)
+
+  g : (n : ℕ) → G n → ℕ
+  g zero b0 = zero
+  g (suc n) (b1 fn⇓ gfn⇓) = suc (g (f n fn⇓) gfn⇓)
+
+-- OK. Now we can prove some theorems about `f` and `g`
+-- without postulating their totality.
+-- The trick is that the theorems say "the statement is true on condition
+-- that the argument belongs to the function's domain.
+
+f3⇓ : F 3
+f3⇓ = a1 (b1 (a1 b0 a0) (b1 a0 b0)) (a1 (b1 a0 b0) (a1 b0 a0))
+
+f3≡3 : f 3 f3⇓ ≡ 3
+f3≡3 = refl
+
+mutual
+
+  fn≡n : ∀ n → (fn⇓ : F n) → f n fn⇓ ≡ n
+  fn≡n zero a0 = refl
+  fn≡n (suc n) (a1 gn⇓ fgn⇓) = cong suc (
+    f (g n gn⇓) fgn⇓
+      ≡⟨ fn≡n (g n gn⇓) fgn⇓ ⟩
+    (g n gn⇓)
+      ≡⟨ gn≡n n gn⇓ ⟩
+    n ∎)
+
+  gn≡n : ∀ n → (gn⇓ : G n) → g n gn⇓ ≡ n
+  gn≡n zero b0 = refl
+  gn≡n (suc n) (b1 fn⇓ gfn⇓) = cong suc (
+    g (f n fn⇓) gfn⇓
+      ≡⟨ gn≡n (f n fn⇓) gfn⇓ ⟩
+    f n fn⇓
+      ≡⟨ fn≡n n fn⇓ ⟩
+    n ∎)
+
+-- However, we can (formally) prove that `f` and `g` are total!
+
+mutual
+
+  all-f : ∀ n → F n
+  all-f zero = a0
+  all-f (suc n) = a1 gn⇓ fgn⇓ where
+    gn⇓ : G n
+    gn⇓ = all-g n
+    fgn⇓ : F (g n gn⇓)
+    fgn⇓ rewrite gn≡n n gn⇓ = all-f n
+
+  all-g : ∀ n → G n
+  all-g zero = b0
+  all-g (suc n) = b1 fn⇓ gfn⇓ where
+    fn⇓ : F n
+    fn⇓ = all-f n
+    gfn⇓ : G (f n fn⇓)
+    gfn⇓ rewrite fn≡n n fn⇓ = all-g n
+
+-- And now we can write down "normal" definition of `f` and `g` that
+-- do not take additional arguments.
+
+total-f : ℕ → ℕ
+total-f n = f n (all-f n)
+
+total-g : ℕ → ℕ
+total-g n = g n (all-g n)
+
+-- And we can prove some theorems about `total-f` and `total-g`.
+-- (Without specifying the domains of `f` and `g`.)
+
+tf5≡0 : total-f 5 ≡ 5
+tf5≡0 = refl
+
+tfn≡n : ∀ n → total-f n ≡ n
+tfn≡n n = fn≡n n (all-f n)