[Agda] Symmetry
Jacques Carette
carette at mcmaster.ca
Fri May 4 18:01:08 CEST 2018
I have a Ph.D. student actively looking into deriving various 'free'
things from theories. Term languages and term orders are included. No
tool available yet, but I'm hopeful we'll have something by the fall.
Jacques
On 2018-05-04 11:55 AM, Philip Wadler wrote:
> 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
> <mailto: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
> <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
> <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/
> <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 <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> <https://lists.chalmers.se/mailman/listinfo/agda>
> >
>
>
>
>
> 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/febe6256/attachment.html>
More information about the Agda
mailing list