如何在Coq中定义自定义tripored类型的相等性？

Hey there! Let's walk through how to handle equality for your tripored type in Coq. Since tripored is just a nested product of trans values (trans * trans * trans), we have two practical approaches to define and use equality for it:

1. Use Coq's Built-in Equality (=) #

Coq natively supports equality for product types—this is the simplest and most straightforward option. For two tripored values to be equal, all their corresponding components must be equal. You can formalize this equivalence with a lemma to make it easier to reason about in proofs:

Lemma tripored_eq_char : forall t1 t2 : tripored,
  t1 = t2 <-> (qt t1 = qt t2) /\ (wt t1 = wt t2) /\ (tt t1 = tt t2).
Proof.
  intros t1 t2. split.
  - (* Forward direction: If triporeds are equal, their components are equal *)
    intro H. inversion H; split; split; reflexivity.
  - (* Reverse direction: If all components are equal, triporeds are equal *)
    intro [Hq [Hw Ht]]. 
    destruct t1 as [[qt1 wt1] tt1]; destruct t2 as [[qt2 wt2] tt2].
    rewrite Hq, Hw, Ht. reflexivity.
Qed.

This lemma lets you convert between equality of tripored values and equality of their individual qt, wt, and tt components whenever you need to in proofs. Coq's built-in rewrite and reflexivity tactics work seamlessly with the native = operator for your product type.

2. Define a Custom Equivalence Relation (For Specialized Use Cases) #

If you ever need a more tailored equality (e.g., ignoring certain components for an equivalence class), you can define a custom propositional equality:

Definition tripored_custom_eq (t1 t2 : tripored) : Prop :=
  (qt t1 = qt t2) /\ (wt t1 = wt t2) /\ (tt t1 = tt t2).

To use this as a proper equivalence relation, you'll want to prove it satisfies the three core properties (reflexivity, symmetry, transitivity):

Lemma tripored_custom_eq_refl : forall t : tripored, tripored_custom_eq t t.
Proof. intros t. split; split; reflexivity. Qed.

Lemma tripored_custom_eq_sym : forall t1 t2 : tripored,
  tripored_custom_eq t1 t2 -> tripored_custom_eq t2 t1.
Proof. intros t1 t2 [Hq [Hw Ht]]. split; split; symmetry; assumption. Qed.

Lemma tripored_custom_eq_trans : forall t1 t2 t3 : tripored,
  tripored_custom_eq t1 t2 -> tripored_custom_eq t2 t3 -> tripored_custom_eq t1 t3.
Proof.
  intros t1 t2 t3 [Hq1 [Hw1 Ht1]] [Hq2 [Hw2 Ht2]].
  split; split;
  - transitivity (qt t2); assumption.
  - transitivity (wt t2); assumption.
  - transitivity (tt t2); assumption.
Qed.

Key Note #

For most standard use cases, Coq's native = is sufficient—our first lemma proves it's exactly equivalent to the custom component-wise equality we defined. The custom approach only makes sense if you need to modify the equality condition later (e.g., relax component equality to some other relation).

内容的提问来源于stack exchange，提问作者Frank Sheng