CS计算机代考程序代写 module 747Induction where

module 747Induction where

— Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

— PLFA coverage of identity, associativity, commutativity, distributivity.

— An example of the associative law for addition, presented using equational reasoning.

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
begin
(3 + 4) + 5
≡⟨⟩
7 + 5
≡⟨⟩
12
≡⟨⟩
3 + 9
≡⟨⟩
3 + (4 + 5)

— A theorem easy to prove.

+-identityᴸ : ∀ (m : ℕ) → zero + m ≡ m
+-identityᴸ m = refl

— A first nontrivial theorem.
— An equational proof is shown in PLFA.
— Instead we will use ‘rewrite’.

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero = refl
+-identityʳ (suc m) rewrite +-identityʳ m = refl

— PLFA’s proof uses helpers cong and sym imported from the standard library,
— and a form of equational reasoning that allows more elaborate justification than above.
— We can use cong in place of rewrite.

+-identityʳ′ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ′ zero = refl
+-identityʳ′ (suc m) = cong suc (+-identityʳ′ m)

— Associativity of addition.
— (Done first in PLFA.)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = refl
+-assoc (suc m) n p = cong suc(+-assoc m n p)

— A useful lemma about addition.
— Equational proof shown in PLFA.

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n = refl
+-suc (suc m) n rewrite +-suc m n = refl

— Commutativity of addition.
— Equational proof shown in PLFA.

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm zero n rewrite +-identityʳ n = refl
+-comm (suc m) n rewrite +-suc n m | +-comm m n = refl

— 747/PLFA exercise: AddSwap (1 point)
— Please do this without using induction/recursion.

+-swap : ∀ (m n p : ℕ) → (m + n) + p ≡ n + (m + p)
+-swap m n p rewrite +-comm m n | +-assoc n m p = refl

— 747/PLFA exercise: AddDistMult (2 points)
— Show that addition distributes over multiplication.

*-+-rdistrib : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-+-rdistrib zero n p = refl
*-+-rdistrib (suc m) n p rewrite +-suc m n | *-+-rdistrib m n p | +-swap (m * p) (n * p) p | +-assoc p (m * p) (n * p) = refl

— 747/PLFA exercise: MultAssoc (2 points)
— Show that multiplication is associative.

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p = refl
*-assoc (suc m) n p rewrite +-suc m n | *-+-rdistrib n (m * n) p | *-assoc m n p = refl

— 747/PLFA exercise: MultComm (3 points)
— Show that multiplication is commutative.
— As with the addition proof above, helper lemmas will be needed.

*-identityʳ : ∀ (m : ℕ) → m * zero ≡ zero
*-identityʳ zero = refl
*-identityʳ (suc m) rewrite *-identityʳ m = refl

*-n*1 : ∀ (m : ℕ) → m * 1 ≡ m
*-n*1 zero = refl
*-n*1 (suc m) rewrite *-n*1 m = refl

*-n*0 : ∀ (m : ℕ) → m * 0 ≡ 0
*-n*0 zero = refl
*-n*0 (suc m) rewrite *-n*0 m = refl

*-suc : ∀ (m n : ℕ) → n * suc m ≡ n + (n * m)
*-suc zero n rewrite *-n*1 n | *-n*0 n | +-identityʳ n = refl
*-suc (suc m) n = {!!}

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm zero n rewrite *-identityʳ n = refl
*-comm (suc m) n rewrite +-comm n (suc m) | *-+-rdistrib 1 m n = {!!}

— 747/PLFA exercise: LeftMonusZero (1 point)
— PLFA asks “Did your proof require induction?”
— (which should give you an indication of the expected answer).

0∸n≡0 : ∀ (m : ℕ) → zero ∸ m ≡ zero
0∸n≡0 zero = refl
0∸n≡0 (suc m) = refl

— 747/PLFA exercise: MonusAssocish (2 points)
— Show a form of associativity for monus.

∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc zero n p rewrite 0∸n≡0 (n + p) = {!!}
∸-+-assoc (suc m) n p = {!!}

— PLFA exercise (stretch): distributive and associative laws for exponentiation.

— 747 extended exercise: properties of binary representation.
— This is based on the PLFA Bin-laws exercise.

— Copied from 747Naturals.

data Bin-ℕ : Set where
bits : Bin-ℕ
_x0 : Bin-ℕ → Bin-ℕ
_x1 : Bin-ℕ → Bin-ℕ

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc n) = suc (suc (dbl n))

— Copy your versions of ‘inc’, ‘to’, ‘from’, ‘bin-+’ over from 747Naturals.
— You may choose to change them here to make proofs easier.
— But make sure to test them if you do!

inc : Bin-ℕ → Bin-ℕ
inc bits = bits x1
inc (m x0) = m x1
inc (m x1) = inc (m) x0

tob : ℕ → Bin-ℕ
tob zero = bits
tob (suc m) = inc (tob m)

fromb : Bin-ℕ → ℕ
fromb bits = 0
fromb (m x0) = dbl (fromb m)
fromb (m x1) = suc (dbl (fromb m))

_bin-+_ : Bin-ℕ → Bin-ℕ → Bin-ℕ
bits bin-+ n = n
(m x0) bin-+ bits = m x0
(m x0) bin-+ (n x0) = (m bin-+ n) x0
(m x0) bin-+ (n x1) = (m bin-+ n) x1
(m x1) bin-+ bits = m x1
(m x1) bin-+ (n x0) = (m bin-+ n) x1
(m x1) bin-+ (n x1) = (inc(m) bin-+ n) x0

— 747 exercise: DoubleB (1 point)
— Write the Bin-ℕ version of dbl, here called dblb.
— As with the other Bin-ℕ operations, don’t use tob/fromb.

dblb : Bin-ℕ → Bin-ℕ
dblb bits = bits
dblb (m x0) = dblb (m) x0
dblb (m x1) = inc (dblb m) x0

— Here are some properties of tob/fromb/inc suggested by PLFA Induction.
— Please complete the proofs.

— 747 exercise: FromInc (1 point)

from∘inc : ∀ (m : Bin-ℕ) → fromb (inc m) ≡ suc (fromb m)
from∘inc bits = refl
from∘inc (m x0) = refl
from∘inc (m x1) = {!!}

— 747 exercise: FromToB (1 point)

from∘tob : ∀ (m : ℕ) → fromb (tob m) ≡ m
from∘tob zero = refl
from∘tob (suc m) = {!cong (tob m)!}

— 747 exercise: ToFromB (2 points)
— The property ∀ (m : Bin-ℕ) → tob (fromb m) ≡ m cannot be proved.
— Can you see why?
— However, this restriction of it can be proved.

to/from-corr : ∀ (m : Bin-ℕ) (n : ℕ) → m ≡ tob n → fromb m ≡ n
to/from-corr m n m≡tn = {!!}

— Here are a few more properties for you to prove.

— 747 exercise: DblBInc (1 point)

dblb∘inc : ∀ (m : Bin-ℕ) → dblb (inc m) ≡ inc (inc (dblb m))
dblb∘inc m = {!!}

— 747 exercise: ToDbl (1 point)

to∘dbl : ∀ (m : ℕ) → tob (dbl m) ≡ dblb (tob m)
to∘dbl m = {!!}

— 747 exercise: FromDblB (1 point)

from∘dblb : ∀ (m : Bin-ℕ) → fromb (dblb m) ≡ dbl (fromb m)
from∘dblb m = {!!}

— 747 exercise: BinPlusLInc (2 points)
— This helper function translates the second case for unary addition
— suc m + n = suc (m + n)
— into the binary setting. It’s useful in the next proof.
— Hint: induction on both m and n is needed.

bin-+-linc : ∀ (m n : Bin-ℕ) → (inc m) bin-+ n ≡ inc (m bin-+ n)
bin-+-linc m n = {!!}

— 747 exercise: PlusUnaryBinary (2 points)
— This theorem relates unary and binary addition.

to∘+ : ∀ (m n : ℕ) → tob (m + n) ≡ tob m bin-+ tob n
to∘+ m n = {!!}

— This ends the extended exercise.

— The following theorems proved in PLFA can be found in the standard library.

— import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

— Unicode used in this chapter:

{-

∀ U+2200 FOR ALL (\forall, \all)
ʳ U+02B3 MODIFIER LETTER SMALL R (\^r)
′ U+2032 PRIME (\’)
″ U+2033 DOUBLE PRIME (\’)
‴ U+2034 TRIPLE PRIME (\’)
⁗ U+2057 QUADRUPLE PRIME (\’)

-}