[Agda] Sign.+ ◃
Sergei Meshveliani
mechvel at botik.ru
Thu Nov 14 15:37:15 CET 2013
People,
For a certain evident lemma for Integer._*_ and _*n_ = Nat._*_,
I write
-------------------------------------------
+◃ : (n : ℕ) → (Sign.+ ◃ n) ≡ + n
+◃ 0 = refl
+◃ (sucN _) = refl
+n*+q=+m : (m n q : ℕ) → n *n q ≡ m → (+ n) * (+ q) ≡ (+ m)
+n*+q=+m m n q n*q=m =
≡begin (+ n) * (+ q) ≡[ refl ]
Sign.+ ◃ (n *n q) ≡[ cong (_◃_ Sign.+) n*q=m ]
Sign.+ ◃ m ≡[ +◃ m ]
+ m
≡end
-------------------------------------------
The necessity of setting ≡[ +◃ m ] instead of just skipping this line
looks strange, as well as the lemma of +◃.
I suspect that this is due to a particular pattern order in the
implementation for Integer._◃_.
May be it is better to move the pattern with ... zero
to the second place?
Or may be, my code can be simplified?
Thanks,
------
Sergei
More information about the Agda
mailing list