英文:
Proving Transitivity of Pointwise Relations on Lists in Coq
问题
In Agda, it's quite easy to prove that if a relation R is transitive then we can define pointwise transitivity on lists:
open import Data.List
Rel : Set → Set₁
Rel A = A → A → Set
private
variable
A : Set
R : A → A → Set
data Pointwise (R : Rel A) : Rel (List A) where
p-nil : Pointwise R [] []
p-cons : ∀ {x y xs ys} → R x y → Pointwise R xs ys → Pointwise R (x ∷ xs) (y ∷ ys)
Transitive : Rel A → Set
Transitive R = ∀ {x y z} → R x y → R y z → R x z
TransitivePointwise : Transitive R → Transitive (Pointwise R)
TransitivePointwise t p-nil p-nil = p-nil
TransitivePointwise t (p-cons Rxy ps) (p-cons Ryz qs) = p-cons (t Rxy Ryz) (TransitivePointwise t ps qs)
However, in Coq, when trying to achieve the same:
Inductive pointwise {A} (R : A -> A -> Prop) : list A -> list A -> Prop :=
| p_nil : pointwise R nil nil
| p_cons : forall {x y} {xs ys}, R x y -> pointwise R xs ys -> pointwise R (x :: xs) (y :: ys).
Theorem transitive_pointwise : forall {A} R, transitive A R -> transitive (list A) (pointwise R).
Proof.
unfold transitive.
intros.
induction H0.
- assumption.
- (* You're stuck here because you need to recurse on `H0 : pointwise R x y` and `H1 : pointwise R y z` at the same time. *)
-
Qed.
I get stuck because I need to recurse on H0 : pointwise R x y and H1 : pointwise R y z at the same time. I've tried using refine with a fixpoint, but in that case, Coq tells me that the fixpoint is ill-formed. It would also be nice to know why when doing destruct H0, H1, Coq gives me four cases, while Agda only gives two.
英文:
In Agda, it's quite easy to prove that if a relation R is transitive then we can define pointwise transitivity on lists:
open import Data.List
Rel : Set → Set₁
Rel A = A → A → Set
private
variable
A : Set
R : A → A → Set
data Pointwise (R : Rel A) : Rel (List A) where
p-nil : Pointwise R [] []
p-cons : ∀ {x y xs ys} → R x y → Pointwise R xs ys → Pointwise R (x ∷ xs) (y ∷ ys)
Transitive : Rel A → Set
Transitive R = ∀ {x y z} → R x y → R y z → R x z
TransitivePointwise : Transitive R → Transitive (Pointwise R)
TransitivePointwise t p-nil p-nil = p-nil
TransitivePointwise t (p-cons Rxy ps) (p-cons Ryz qs) = p-cons (t Rxy Ryz) (TransitivePointwise t ps qs)
However, in Coq, when trying to achieve the same:
Inductive pointwise {A} (R : A -> A -> Prop) : list A -> list A -> Prop :=
| p_nil : pointwise R nil nil
| p_cons : forall {x y} {xs ys}, R x y -> pointwise R xs ys -> pointwise R (x :: xs) (y :: ys).
Theorem transitive_pointwise : forall {A} R, transitive A R -> transitive (list A) (pointwise R).
Proof.
unfold transitive.
intros.
induction H0.
- assumption.
-
Qed.
I get stuck because I need to recurse on H0 : pointwise R x y and H1 : pointwise R y z at the same time. I've tried using refine with a fixpoint, but in that case, Coq tells me that the fixpoint is ill-formed. It would also be nice to know why when doing destruct H0, H1, Coq gives me four cases, while Agda only gives two.
答案1
得分: 0
Here are the translated parts:
Original:
If you do an induction over lists (instead of over a hypothesis of type pointwise ? ?) and a few calls to inversion, it works.
Translation:
如果你对列表进行归纳（而不是对类型为pointwise ? ?的假设进行归纳），并进行几次inversion调用，它可以工作。
Original:
Ups! You can also induct over Hxy: pointwise x y:
Translation:
哎呀！你也可以对Hxy: pointwise x y进行归纳：
If you need further translations or assistance, please let me know.
英文:
If you do an induction over lists (instead of over an hypothesis of type pointwise ? ?) and a few calls to inversion, it works.
Require Import Relations.
Theorem transitive_pointwise :
forall {A} R, transitive A R -> transitive (list A) (pointwise R).
Proof.
unfold transitive; induction x.
- inversion 1; subst; auto.
- destruct y.
+ inversion 1.
+ inversion 1; subst.
* inversion 1; subst; constructor.
eapply H; eauto.
eapply IHx; eauto.
Qed.
(Edited)
Ups! You can also induct over Hxy: pointwise x y :
Theorem transitive_pointwise' :
forall {A} R, transitive A R -> transitive (list A) (pointwise R).
Proof.
intros A R H x y z Hxy; revert z.
induction Hxy.
- trivial.
- destruct z.
+ inversion 1.
+ inversion 1; subst; constructor.
* eapply H;eauto.
* now apply IHHxy.
Qed.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论