Discussion:
[Agda] Symmetry
Philip Wadler
2018-05-03 11:49:03 UTC
Permalink
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/
James Wood
2018-05-03 21:34:50 UTC
Permalink
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
Post by Philip Wadler
-- 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
  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
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-05-04 15:55:25 UTC
Permalink
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/
Post by 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
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
Post by Philip Wadler
-- 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
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
https://lists.chalmers.se/mailman/listinfo/agda
Jacques Carette
2018-05-04 16:01:08 UTC
Permalink
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
Post by 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/
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
  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
https://gist.github.com/laMudri/8b98b85ce570a09b464c007b1325ca1b
<https://gist.github.com/laMudri/8b98b85ce570a09b464c007b1325ca1b>
     -- 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
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
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
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-05-04 16:09:16 UTC
Permalink
Cool, thanks! -- 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/
Post by Jacques Carette
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
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/
Post by 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
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
Post by Philip Wadler
-- 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
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
https://lists.chalmers.se/mailman/listinfo/agda
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Loading...