[Agda] Proof involving Fin

[Peter Thiemann]

Dear Bradley,

Excellent, that will get me further.

Thanks
-Peter

> On 21. Feb 2018, at 18:05, Bradley Hardy <bch29 at cam.ac.uk> wrote:
> 
> 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
>