I'm having trouble using the string decideability. First, I'm confused why it is so difficult to work with decideability in Agda, when in Coq it seems smooth as butter. When I try to prove this simple theorem about strings, Agda unfolds this mess of a definition which is pretty much impossible to work with unless you know exactly what you are trying to do. How can I work with string decideability via pattern matching that keeps the definition in tact?
Am using Stump's keep function instead of Agda's inspect.
keep : ∀{ℓ}{A : Set ℓ} → (x : A) → Σ A (λ y → x ≡ y)
keep x = ( x , refl )
--first roadblock
eqbStringrefl' : forall (b : String) → true ≡ (b == b)
eqbStringrefl' b with keep (b ≟ b)
eqbStringrefl' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd = {!!}
eqbStringrefl' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = {!!}
Here is Agda's output:
-- Goal: true ≡
-- Relation.Nullary.Decidable.Core.isYes
-- (Relation.Nullary.Decidable.Core.map′
-- (λ x →
-- Agda.Builtin.String.Properties.primStringToListInjective b b
-- (Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
-- (Data.List.Relation.Binary.Pointwise.map
-- (λ {z} {z = z₁} →
-- Agda.Builtin.Char.Properties.primCharToNatInjective z z₁)
-- x)))
-- (λ x →
-- Data.List.Relation.Binary.Pointwise.map
-- (cong Agda.Builtin.Char.primCharToNat)
-- (Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
-- (cong Data.String.toList x)))
-- (Data.List.Relation.Binary.Pointwise.decidable
-- (λ x y →
-- Relation.Nullary.Decidable.Core.map′
-- (Data.Nat.Properties.≡ᵇ⇒≡ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Nat.Properties.≡⇒≡ᵇ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Bool.Properties.T?
-- (Agda.Builtin.Char.primCharToNat x Data.Nat.≡ᵇ
-- Agda.Builtin.Char.primCharToNat y)))
-- (Data.String.toList b) (Data.String.toList b)))
-- ————————————————————————————————————————————————————————————
-- snd : Relation.Nullary.Decidable.Core.map′
-- (λ x →
-- Agda.Builtin.String.Properties.primStringToListInjective b b
-- (Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
-- (Data.List.Relation.Binary.Pointwise.map
-- (λ {z} {z = z₁} →
-- Agda.Builtin.Char.Properties.primCharToNatInjective z z₁)
-- x)))
-- (λ x →
-- Data.List.Relation.Binary.Pointwise.map
-- (cong Agda.Builtin.Char.primCharToNat)
-- (Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
-- (cong Data.String.toList x)))
-- (Data.List.Relation.Binary.Pointwise.decidable
-- (λ x y →
-- Relation.Nullary.Decidable.Core.map′
-- (Data.Nat.Properties.≡ᵇ⇒≡ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Nat.Properties.≡⇒≡ᵇ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Bool.Properties.T?
-- (Agda.Builtin.Char.primCharToNat x Data.Nat.≡ᵇ
-- Agda.Builtin.Char.primCharToNat y)))
-- (Data.String.toList b) (Data.String.toList b))
-- ≡ Relation.Nullary.yes refl
-- b : String
If I now apply a rewrite, the goal is simplified but we still have a mess in the hypothesis list. When I try to ctrl-a, i get the following error, despite the goal being seemingly inferrable:
Goal: true ≡ true
Not implemented: The Agda synthesizer (Agsy) does not support
copatterns yet
Nonetheless, I was able to proceed as if the snd term was significantly cleaner, and then just applying the basic rules to arrive at final proof.
eqbStringrefl'' : forall (b : String) → true ≡ (b == b)
eqbStringrefl'' b with keep (b ≟ b)
eqbStringrefl'' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd rewrite snd = {!!}
eqbStringrefl'' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = {!!}
-- eqbStringrefl'' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd rewrite snd = refl
-- eqbStringrefl'' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = ⊥-elim (¬p refl)
The last line is the completed proof. Any suggestions would be helpful!
