[Agda] Symmetry

[Philip Wadler]

Thanks, James. You note the proof of totality has c^2 easy cases, but it is
no easier than repeating the redundant cases in a proof of determinism.
Your suggestion fails to simplify the proof, but would help if one had more
than one proof where one wished to exploit symmetry, or if one already had
a total order for some other reason. (I expect one could derive a total
order on reductions from a total order on terms, which would also help.)

Sounds like what Agda needs is a tool for deriving lexicographic orders,
*including* a proof that the lexicographic order is a total order. Is
anyone looking at such a tool? I remember Ulf describing how deriving
supports decidable equality.

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/

On 3 May 2018 at 18:34, James Wood <james.wood.100 at strath.ac.uk> wrote:

> 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
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180504/79293f9e/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180504/79293f9e/attachment.ksh>