Discussion:
Proof involving Fin
(too old to reply)
Peter Thiemann
2018-02-21 16:36:49 UTC
Permalink
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) = {!!}
%%%%%%%%%%%%
Bradley Hardy
2018-02-21 17:05:56 UTC
Permalink
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
Post by Peter Thiemann
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
Peter Thiemann
2018-02-21 17:15:38 UTC
Permalink
Dear Bradley,

Excellent, that will get me further.

Thanks
-Peter
Post by 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.
≈-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
Post by Peter Thiemann
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
Loading...