Data.Fin and with statement

[shinji-kono]

I'm using Agda version 2.6.4 and standard-library-2.0

In the fixing a working code in Agda 2.6.3 and standard-library, (simialar one with Data.Fin.Permutation.remove)

   p← : Fin n → Fin n 
   p← x with perm ⟨$⟩ˡ (suc x) in eq
   p← x | zero  = ⊥-elim ( sh2 perm p0=0 {x} eq )
   p← x | suc t = t

   p01 : (x : Fin n) → ?
   p01 x with perm ⟨$⟩ˡ (suc x) 
   ... | t = ?

   bad1 : (x : Fin n) → Fin (suc n)
   bad1 x = perm ⟨$⟩ˡ (suc x) 

   bad : (x : Fin n) → p← x ≡ ?
   bad with bad1 x
   ... | t = ?

This gives me ...

/Users/kono/src/galois/src/pm.agda:60,4-15
Function.Bundles.Inverse.from perm (suc x) != w of type Fin (suc n)
when checking that the type
{n : ℕ} (perm : Permutation (suc n) (suc n)) (x : Fin n)
(w : Fin (suc n))
(p0=0 : Function.Bundles.Inverse.from perm zero ≡ zero) →
(p← perm p0=0 x | w | refl) ≡
?2 (perm = perm) (p0=0 = p0=0) (x = x)
of the generated with function is well-formed

pm.agda

[andreasabel]

I think this isn't a bug in Agda, maybe some inconvenience with the new with...in.... I moved it here because it feels like it belongs into the deprecation of inspect topic.

• Deprecate inspect function in favour of new with ... in construct #1580

Also, I think here is more expertise how to prove stuff about functions defined with with...in....

Here is the code from the OP with polished import statements:

{-# OPTIONS --cubical-compatible --safe #-}
module _ where

open import Data.Fin                              using (Fin; zero; suc; #_)
open import Data.Fin.Permutation                  using (Permutation; _⟨$⟩ˡ_; _⟨$⟩ʳ_; inverseˡ; inverseʳ; permutation)
open import Data.Nat.Base                         using (ℕ; suc; zero; s≤s ; z≤n )
open import Relation.Binary.PropositionalEquality using (_≡_; cong; refl; sym; module ≡-Reasoning)

open import Relation.Nullary                      using (¬_)
open import Data.Empty                            using (⊥-elim)

shlem→ : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
shlem→ perm p0=0 x px=0 = begin
          x                                  ≡⟨ sym ( inverseʳ perm ) ⟩
          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x)           ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) px=0 ⟩
          perm ⟨$⟩ʳ zero                     ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) (sym p0=0) ⟩
          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero)        ≡⟨ inverseʳ perm  ⟩
          zero
       ∎  where open ≡-Reasoning

shlem← : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero
shlem← perm p0=0 x px=0 =  begin
          x                                  ≡⟨ sym (inverseˡ perm ) ⟩
          perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x )          ≡⟨ cong (λ k →  perm ⟨$⟩ˡ k ) px=0 ⟩
          perm ⟨$⟩ˡ zero                     ≡⟨ p0=0  ⟩
          zero
       ∎  where open ≡-Reasoning

sh2 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero
sh2 perm p0=0 {x} eq with shlem→ perm p0=0 (suc x) eq
sh2 perm p0=0 {x} eq | ()

sh1 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero
sh1 perm p0=0 {x} eq with shlem← perm p0=0 (suc x) eq
sh1 perm p0=0 {x} eq | ()


-- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ []
shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
shrink {n} perm p0=0  = permutation p→ p← piso← piso→  where

   p→ : Fin n → Fin n
   p→ x with perm ⟨$⟩ʳ (suc x) in eq
   p→ x | zero  = ⊥-elim ( sh1 perm p0=0 {x} eq )
   p→ x | suc t = t

   p← : Fin n → Fin n
   p← x with perm ⟨$⟩ˡ (suc x) in eq
   p← x | zero  = ⊥-elim ( sh2 perm p0=0 {x} eq )
   p← x | suc t = t

   abbrv : (x : Fin n) → Fin (suc n)
   abbrv x = perm ⟨$⟩ˡ (suc x)

   --  using "with" something bound in ≡ is prohibited
   piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
   piso← x = {!!}

   piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
   piso→ x = {!!}

   p01 : (x : Fin n) →  p→ ( p← x ) ≡ x
   p01 x with perm ⟨$⟩ˡ (suc x) in eq
   ... | t = {!!}

The task is to prove piso←, and p01 is a draft that does not work because with-abstraction does not do the right thing here.

If I wanted to make progress on this, I probably would reformulate p→ in terms of the inspect idiom and then see if I get the correct magic with incantation.

[jamesmckinna]

Ha! Thanks to each of @Taneb and @andreasabel for this... but I might also wish to loop @gallais and even notorious with-sceptic @omelkonian (sorry Orestis!) into the discussion for moral support...

Meanwhile, my continuing tracking of @omelkonian 's issues in the main Agda issue tracker have led me to the (reluctant!) conclusion that we

• continue to eliminate uses of inspect from the library;
• BUT, abandon its deprecation for the time being...

Meanwhile, I'll scratch my head a bit harder about this example, and throw back to the main developers the question concerning how inspect enjoys its own peculiar sweet spot of strict/non-strictness in terms of matching on refl... cf. agda/agda#5833

[jamesmckinna]

The other thing to ask for here @shinji-kono is the original working version of the code under 2.6.3/stdlib-v?.?.?, again in as cleaned-up a state as possible. Thanks!

UPDATED: looking over the code for Data.Fin.Permutation.remove (which does typecheck under Agda-v2.6.3/stdlib-v2.0) I'm mystified... the structure of those proofs is very different from your approach. Can you account for the differences?

[MatthewDaggitt]

@jamesmckinna did one of the PRs fix this or is this still an outstanding problem?

[jamesmckinna]

@MatthewDaggitt wrote:

@jamesmckinna did one of the PRs fix this or is this still an outstanding problem?

This is still outstanding, AFAIU. (And I have not solved the problem, except see below)

I requested a look at the original code said to be working under 2.6.3, but have yet to see it. The definition of remove in Data.Fin.Permutationdoes typecheck under 2.6.3 (I haven't checked under 2.6.4, but I presume it must given all the other checks being carried out under v2.6.4/v2.0) so I'm not completely clear what the exact issue is.

Saying something "doesn't work" using with ... in seems moot (to me, at least; and at least for the time being, while we try to finish the v2.0 release...) since we undeprecated inspect #2107 #2128 But it's possible that I have not actually understood the original problem well enough. In any case,

shrink = remove zero perm

seems a solution to the definitional problem. As would the followup of going through the definition of remove and specialising it to the case remove zero. NB the whole Data.Fin.Permutation module makes clear that the additional degree of freedom which arises from taking Permutation m n for distinct indices m, n (even though the mathematics ensures that m ≡ n is provable) is useful/important, so again it is not obvious to me that specialising to the case of m = n on-the-nose is even the right thing to do here, either?

@andreasabel , @shinji-kono do you think that this is a problem that still concerns agda-stdlib-v2.0? It seems to me that this is about the ergonomics/pragmatics of with... in..., ie an agda issue, rather than a agda-stdlib issue. If so, suggest that we close this here remove this from the v2.0 milestone, or move back to the main issue tracker.

The fact that the proposed 'solution' via p→/p← and piso←/piso→ "does not work" (again I ask: did it before? if so, how?) using with... in ... may, sadly, be further evidence that @gallais design/implementation of the latter is not (yet) quite right for all users' needs. But as I have already indicated above, the actual (working!) definition of remove is much more subtle... and perhaps it might be simplifiable in this instance, but I have no grounds for believing that at this point.

As for the general case of remove, which involves a great deal of punchIn/punchOut reasoning on Fin (again, AFAIU, due to @TOTBWF ), I draw people's attention to my specimen PR #1921 ... and suggest that the iso proofs might yield to a view-based analysis of the functions p→/p←, but again, I have no grounds either way to judge that (other than instincts), and don't have the cycles/bandwidth to devote to it right now. Sorry!

[jamesmckinna]

@MatthewDaggitt TL;DR : suggest we close move this to Agda-future, unless this really is a bug in either agda-v2.6.4 or agda-stdlib-v2.0?

[MatthewDaggitt]

Yup I agree with your analysis. Unless @shinji-kono can provide us with code that works in v1.7 and not in v2.0, then I think the evidence suggests they're simply running into a shortcoming of with ... in.

Will close, but @shinji-kono feel free to post proof your code worked with the previous version of the standard library and Agda, in which case we'll reopen it.