• API
• FAQ
• Tools
• Archive
daily pastebin goal
2%
SHARE
TWEET

# Cancellation of snoc

a guest Dec 16th, 2018 70 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.

Top