[Agda] Proof involving Fin

[Bradley Hardy]

Dear Peter,

Agda often doesn’t like pattern matching or rewriting on type equalities where the same variable appears in both sides.

To get around this issue, it helps to use heterogeneous equality. The standard library defines a general version, but here’s a type specific to `Fin` that should be easier to understand.

data _≈_ {m} : ∀ {n} → Fin m → Fin n → Set where
  reflexive : {i j : Fin m} → i ≡ j → i ≈ j

cong-suc : ∀ {m n} {i : Fin m} {j : Fin n} → i ≈ j → suc i ≈ suc j
cong-suc (reflexive p) = reflexive (cong suc p)

You can see how it’s possible to write `i ≈ j` even when `i` and `j` are from finite sets of different sizes. Now an analogous theorem to yours is easy to prove.

inject+0n : ∀ {n : ℕ} (fn : Fin n) → inject+ 0 fn ≈ fn
inject+0n {zero} ()
inject+0n {suc n} zero rewrite n+0=n n = reflexive refl
inject+0n {suc n} (suc fn) = cong-suc (inject+0n fn)

Notice the rewrite on `n+0=n n` to convince Agda that it is valid to introduce the `reflexive` constructor.

We can retrieve propositional equality like this:

≈-n≡m : ∀ {m n} {i : Fin m} {j : Fin n} → i ≈ j → m ≡ n
≈-n≡m (reflexive _) = refl

≈-to-≡ : ∀ {m n} {i : Fin m} {j : Fin n} (p : i ≈ j) → subst Fin (≈-n≡m p) i ≡ j
≈-to-≡ (reflexive p) = p

inject+0n′ : ∀ {n : ℕ} (fn : Fin n) → subst Fin (≈-n≡m (inject+0n fn)) (inject+ 0 fn) ≡ fn
inject+0n′ fn = ≈-to-≡ (inject+0n fn)

I hope this helps!

-Bradley

> On 21 Feb 2018, at 16:36, Peter Thiemann <thiemann at informatik.uni-freiburg.de> wrote:
> 
> Dear list,
> 
> I’m stuck with a proof involving the Fin module from the standard library.
> I need to use Data.Fin.inject+ and the last definition is the lemma that I need.
> However, when I try to solve the first hole by pattern matching on the argument of coerce list this:
> 
> inject+0n {suc n} zero with finn=n+0 n
> ... | p = {!!}
> 
> But then I cannot destruct p because its type is 
> p : Fin n ≡ Fin (n + 0)
> 
> That ought to be fixable with a rewrite, but all alternatives I tried were rejected by Agda.
> 
> -Peter
> 
> 
> %%%%%%%%%%%%
> module Lemmas where
> 
> open import Data.Fin hiding (_+_ ; _≤_)
> open import Data.Nat
> open import Relation.Binary.PropositionalEquality
> 
> 
> -- about Fin and Nat
> n=n+0 : (n : ℕ) → n ≡ n + 0
> n=n+0 zero = refl
> n=n+0 (suc n) = cong suc (n=n+0 n)
> 
> n+0=n : (n : ℕ) → n + 0 ≡ n
> n+0=n zero = refl
> n+0=n (suc n) = cong suc (n+0=n n)
> 
> m=n=>finm=finn : ∀ {m n : ℕ} → m ≡ n → Fin m ≡ Fin n
> m=n=>finm=finn refl = refl
> 
> finn=n+0 : (n : ℕ) → Fin n ≡ Fin (n + 0)
> finn=n+0 n = m=n=>finm=finn (n=n+0 n)
> 
> coerce : ∀ {A B : Set} → A ≡ B → A → B
> coerce refl x = x
> 
> inject+0n : ∀ {n : ℕ} (fn : Fin n) → inject+ 0 fn ≡ coerce (finn=n+0 n) fn
> inject+0n {zero} ()
> inject+0n {suc n} zero = {!!}
> inject+0n {suc n} (suc fn) = {!!}
> %%%%%%%%%%%%
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180221/cdb6489a/attachment-0001.html>