CODEWITHSUNDEEP
proofagdaagda-mode
Max Podpera
Max Podpera

Reputation: 59

Agda Recursion on Proof

I have created a recursive Datatype „Positive“ in Agda. Im using this datatype to Index some Tree. On those trees I am trying to proof that a set operation on some Index q doesnt affect a get operation (result) from another index p.

gso : {A : Set} -> ∀ (i j : Positive) (t : Tree A) (v : A) → ((i ≡ j) → ⊥) → get i (set j v t) ≡ get i t
gso (xI p) (xI p) t v = ? 
gso (xO p) (xO p) t v = ?
gso p q t v = ? -- this works fine

I tried splitting up the different cases for the tree into this

gso (xI p) (xI q) (Nodes (node001 t)) v neq = gso p q (Nodes t) v neq

But here i get the error:

p != (xI p) of type Positive
when checking that the expression neq has type p ≡ q → ⊥

or if I remove the neq from calling the proof:

(p ≡ q → ⊥) → get p (set q v (Nodes t)) ≡ get p (Nodes t) !=<
get (xI p) (set (xI q) v (Nodes (node001 t))) ≡
get (xI p) (Nodes (node001 t))
when checking that the expression gso p q (Nodes t) v has type
get (xI p) (set (xI q) v (Nodes (node001 t))) ≡
get (xI p) (Nodes (node001 t))

**My question now is why doesn't Agda understand this step and how can i make it more obvious to Agda? Or what do i understand wrong with using the proof **

Thank you for any help you can provide.

I tried creating a proof that ≡ stays the same with added constructors / steps. But I run into the same error here.

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_)
open Eq.≡-Reasoning


data Positive : Set where 
    xH : Positive
    xI : Positive -> Positive
    xO : Positive -> Positive

proof : ∀ (p q : Positive) → (p ≡ q) → ((xI p) ≡ (xI q))
proof xH xH = λ _ → refl
proof (xI p) xH = λ ()
proof (xO p) xH = λ ()  
proof xH (xI q) = λ ()
proof (xI p) (xI q) = proof p q -- This is where i run into the error again   
proof (xO p) (xI q) = λ ()
proof xH (xO q) = λ () 
proof (xI p) (xO q) = λ ()
proof (xO p) (xO q) = ?

This is also a minimal example that can be executed to run into my problem.

Upvotes: 0

Views: 47

Answers (1)

Max Podpera
Max Podpera

Reputation: 59

I solved this by replacing the definition of the proof with:

gso : {A : Set} → ∀ (i j : Positive) (t : Tree A) (v : A) → (i ≠ j) → (get i (set j v t) ≡ get i t)

where „≠" is defined as

  data _≠_ : Positive → Positive → Set where 
    i≠o : ∀ {p q : Positive} → (xI p) ≠ (xO q)
    o≠i : ∀ {p q : Positive} → (xO p) ≠ (xI q)
    i≠i : ∀ {p q : Positive} → p ≠ q → (xI p) ≠ (xI q)
    o≠o : ∀ {p q : Positive} → p ≠ q → (xO p) ≠ (xO q)

the proofs can then be written as:

  gso (xI p) (xI q) Empty v (i≠i x) = gso p q Empty v x

Upvotes: 0

Related Questions