[Agda] Symmetry

[James Wood]

I believe I've done the same sort of thing before by introducing a
(constructively) total ordering between the things that should be
handled symmetrically. I'm not sure whether it really is helpful, but it
might be worth a try. I wrote up a simplified example at [0], which I'll
explain the approach of here.

First, introduce a relation _≤_ : ∀ {M M′ M″} → (M ⟶ M′) → (M ⟶ M″) →
Set, and prove total : ∀ {M M′ M″} → (r0 : M ⟶ M′) (r1 : M ⟶ M″) → r0 ≤
r1 ⊎ r1 ≤ r0. The relation _≤_ should roughly be what deriving Ord would
give in Haskell, though all of the data in the _⟶_ constructors except
inductive positions can be ignored for simplicity. For example, if you
wanted this relation to be over List A, the definition could be:

  data _≤_ : (xs ys : List A) → Set where
    []≤[] : [] ≤ []
    []≤∷ : ∀ {x xs} → [] ≤ x ∷ xs
    ∷≤∷ : ∀ {x y xs ys} → xs ≤ ys → x ∷ xs ≤ y ∷ ys

This does not assume any ordering on A. Notice that this definition will
have tr(c) constructors, where c is the number of constructors of the
original type (List, _⟶_).

Next, prove the lemma det-≤ : ∀ {M M′ M″} (r0 : M ⟶ M′) (r1 : M ⟶ M″) →
r0 ≤ r1 → M′ ≡ M″ by induction on the proof of r0 ≤ r1. This will
essentially contain only the cases you wanted to write, with no
duplicates. From this, the desired result det is proved by cases on
total r0 r1, using det-≤ in both cases (and sym in the second case).

The bottleneck in this is the proof of total, which requires the full c²
cases. However, this should be an easy proof. Wherever the two head
constructors differ, C-c C-a should find the solution, and the c-many
diagonal cases are by congruence.

James

[0]: https://gist.github.com/laMudri/8b98b85ce570a09b464c007b1325ca1b

On 03/05/18 12:49, Philip Wadler wrote:
> Here is a proof that reduction is deterministic:
> 
>     -- Values do not reduce
>     Val-⟶ : ∀ {M N} → Value M → ¬ (M ⟶ N)
>     Val-⟶ Fun ()
>     Val-⟶ Zero ()
>     Val-⟶ (Suc VM) (ξ-suc M⟶N)  =  Val-⟶ VM M⟶N
> 
> 
>     -- Reduction is deterministic 
> 
>     det : ∀ {M M′ M″}
>       → (M ⟶ M′)
>       → (M ⟶ M″)
>         ----------
>       → M′ ≡ M″
>     det (ξ-·₁ L⟶L′) (ξ-·₁ L⟶L″) =  cong₂ _·_ (det L⟶L′ L⟶L″) refl
>     det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL L⟶L′)
>     det (ξ-·₁ L⟶L′) (β-→ _) = ⊥-elim (Val-⟶ Fun L⟶L′)
>     det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL L⟶L″)
>     det (ξ-·₂ _ M⟶M′) (ξ-·₂ _ M⟶M″) = cong₂ _·_ refl (det M⟶M′ M⟶M″)
>     det (ξ-·₂ _ M⟶M′) (β-→ VM) = ⊥-elim (Val-⟶ VM M⟶M′)
>     det (β-→ VM) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ Fun L⟶L″)
>     det (β-→ VM) (ξ-·₂ _ M⟶M″) = ⊥-elim (Val-⟶ VM M⟶M″)
>     det (β-→ _) (β-→ _) = refl
>     det (ξ-suc M⟶M′) (ξ-suc M⟶M″) = cong `suc_ (det M⟶M′ M⟶M″)
>     det (ξ-pred M⟶M′) (ξ-pred M⟶M″) = cong `pred_ (det M⟶M′ M⟶M″)
>     det (ξ-pred M⟶M′) β-pred-zero = ⊥-elim (Val-⟶ Zero M⟶M′)
>     det (ξ-pred M⟶M′) (β-pred-suc VM) = ⊥-elim (Val-⟶ (Suc VM) M⟶M′)
>     det β-pred-zero (ξ-pred M⟶M′) = ⊥-elim (Val-⟶ Zero M⟶M′)
>     det β-pred-zero β-pred-zero = refl
>     det (β-pred-suc VM) (ξ-pred M⟶M′) = ⊥-elim (Val-⟶ (Suc VM) M⟶M′)
>     det (β-pred-suc _) (β-pred-suc _) = refl
>     det (ξ-if0 L⟶L′) (ξ-if0 L⟶L″) = cong₃ `if0_then_else_ (det L⟶L′
>     L⟶L″) refl refl
>     det (ξ-if0 L⟶L′) β-if0-zero = ⊥-elim (Val-⟶ Zero L⟶L′)
>     det (ξ-if0 L⟶L′) (β-if0-suc VL) = ⊥-elim (Val-⟶ (Suc VL) L⟶L′)
>     det β-if0-zero (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶ Zero L⟶L″)
>     det β-if0-zero β-if0-zero = refl
>     det (β-if0-suc VL) (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶ (Suc VL) L⟶L″)
>     det (β-if0-suc _) (β-if0-suc _) = refl
>     det (ξ-Y M⟶M′) (ξ-Y M⟶M″) = cong `Y_ (det M⟶M′ M⟶M″)
>     det (ξ-Y M⟶M′) (β-Y refl) = ⊥-elim (Val-⟶ Fun M⟶M′)
>     det (β-Y refl) (ξ-Y M⟶M″) = ⊥-elim (Val-⟶ Fun M⟶M″)
>     det (β-Y refl) (β-Y refl) = refl
> 
> 
> The proof and all relevant definitions are here:
>   https://wenkokke.github.io/sf/Typed
> 
> Almost half the lines in the above proof are redundant, for example
> 
>     det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL L⟶L′)
>     det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL L⟶L″)
> 
>  
> are essentially identical.
> 
> What I would like to do is delete the redundant lines and add
> 
>     det M⟶M′ M⟶M″ = sym (det M⟶M″ M⟶M′)
> 
> 
> to the bottom of the proof. But, of course, the termination checker
> complains.
> 
> How can I rewrite the proof to exploit symmetry? Cheers, -- P
> 
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
> 
> 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>