daily pastebin goal
15%
SHARE
TWEET

Cancellation of snoc

a guest Dec 16th, 2018 73 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Theorem “Cancellation of ▹”:
  2.     xs ▹ x = ys ▹ y  ≡  xs = ys ∧ x = y
  3. Proof:
  4.   By induction on `xs : Seq A`:
  5.     Base case:
  6.       By induction on `ys : Seq A`:
  7.         Base case:
  8.             𝜖 ▹ x = 𝜖 ▹ y  ≡  𝜖 = 𝜖 ∧ x = y
  9.           =⟨ “Definition of ▹ for 𝜖” ⟩
  10.             x ◃ 𝜖 = y ◃ 𝜖  ≡  𝜖 = 𝜖 ∧ x = y
  11.           =⟨ “Cancellation of ◃” ⟩
  12.             𝜖 = 𝜖 ∧ x = y  ≡  𝜖 = 𝜖 ∧ x = y
  13.           ≡⟨ “Reflexivity of ≡” ⟩
  14.             true
  15.         Induction step:
  16.           For any `c`:
  17.               𝜖 ▹ x = (c ◃ ys) ▹ y  
  18.             =⟨ “Definition of ▹ for 𝜖” ⟩
  19.               x ◃ 𝜖 = (c ◃ ys) ▹ y  
  20.             =⟨ “Definition of ▹ for ◃” ⟩
  21.               x ◃ 𝜖 = c ◃ (ys ▹ y)
  22.             =⟨ “Cancellation of ◃” ⟩
  23.               x = c ∧ 𝜖 = (ys ▹ y)
  24.             =⟨ “Snoc is not empty” ⟩
  25.               x = c ∧ false
  26.             =⟨ “Zero of ∧” ⟩
  27.               false
  28.             =⟨ “Cons is not empty”, “Zero of ∧” ⟩
  29.               𝜖 = (c ◃ ys) ∧ x = y
  30.     Induction step:
  31.       For any `d`:
  32.         By induction on `ys : Seq A`:
  33.           Base case:
  34.               (d ◃ xs) ▹ x = 𝜖 ▹ y  ≡  
  35.               (d ◃ xs) = 𝜖 ∧ x = y
  36.             =⟨ “Cons is not empty”, “Zero of ∧” ⟩
  37.               (d ◃ xs) ▹ x = 𝜖 ▹ y  ≡  false
  38.             =⟨ “Definition of ▹ for 𝜖”,
  39.               “Definition of ▹ for ◃” ⟩
  40.               d ◃ (xs ▹ x) = y ◃ 𝜖  ≡  false
  41.             =⟨ “Cancellation of ◃” ⟩
  42.               d = y ∧ (xs ▹ x) = 𝜖  ≡  false
  43.             =⟨ “Snoc is not empty”, “Zero of ∧” ⟩
  44.               false ≡ false
  45.             =⟨ “Reflexivity of ≡” ⟩
  46.               true
  47.           Induction step:
  48.             For any `a`:
  49.                 (d ◃ xs) ▹ x = (a ◃ ys) ▹ y
  50.               =⟨ “Definition of ▹ for ◃” ⟩
  51.                 d ◃ (xs ▹ x) = a ◃ (ys ▹ y)
  52.               =⟨ “Cancellation of ◃” ⟩
  53.                 a = d ∧ (xs ▹ x) = (ys ▹ y)
  54.               =⟨ Induction hypothesis
  55.                  `xs ▹ x = ys ▹ y  ≡  xs = ys ∧ x = y` ⟩
  56.                 a = d ∧ xs = ys ∧ x = y
  57.               =⟨ “Cancellation of ◃” ⟩
  58.                 (d ◃ xs) = (a ◃ ys) ∧ x = y
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top