Я пытаюсь доказать, что вычитание nat, которое я определил с помощью рекурсора, действительно является функцией вычитания. Ниже у меня есть правильное, fucntion - , и тот, который я построил, правильно тестирует, но не дает рефлексивного доказательства ключевого свойства дефинитонального равенства (su c m - su c n = m - n).
Кроме того, друг поделился со мной своим рекурсором, который работает, ∸ .
Почему моя функция вычитания проходит тест, но не удалось доказать результат? Это правильно.
module subtract where
open import Data.Nat using (ℕ; _+_; suc; zero; _*_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst; trans; sym)
open import Data.Product using ( _×_; Σ; Σ-syntax; _,_; proj₁; proj₂ )
open import Data.List using (List; _∷_; []; map; concat; [_])
_-_ : ℕ → ℕ → ℕ
zero - n = zero
suc m - zero = suc m
suc m - suc n = m - n
rec : {C : Set} → (N : C) → ((x : ℕ) → (y : C) → C) → (M : ℕ) → C
rec N _ zero = N
rec N P' (suc M) = P' M (rec N P' M)
pred : ℕ → ℕ
pred n = rec zero (λ x y → x) n
_-'_ : ℕ → ℕ → ℕ
m -' n = rec zero (λ x y → rec m (λ x₁ y₁ → pred y₁) n) m
-- this works
_∸_ : ℕ → ℕ → ℕ
_∸_ = rec (λ z → z) λ m r → rec (suc m) (λ n _ → r n)
∸-lem : ∀ (m n) → (suc m ∸ suc n) ≡ (m ∸ n)
∸-lem m n = refl
-- fail, even though it passes the test below
-'-lem : ∀ (m n) → (suc m -' suc n) ≡ (m -' n)
-'-lem m n = {!refl!}
-- testing
oneToN : ℕ → List ℕ
oneToN zero = []
oneToN (suc x) = suc x ∷ oneToN x
1to100 = oneToN 10
pairs-help : {A B : Set} → List A → B → List (B × A)
-- pairs-help xs y = Data.List.map (λ x → y , x ) xs
pairs-help xs y = Data.List.map (λ x → y , x ) xs
product-list = concat (Data.List.map (pairs-help 1to100) 1to100 )
appPair : {A : Set} → (A → A → A) → A × A → A
appPair f (fst , snd) = f fst snd
test- = map (appPair _-_) product-list
test-' = map (appPair _-'_) product-list
leq : test- ≡ test-'
leq = refl