Set Implicit Arguments.
Require Import Coq.Program.Equality.
Require Import MyTactics.
Section lexicographic_product.
Variable A :
Type.
Variable B :
Type.
Variable eqA :
A ->
A ->
Prop.
Variable lessA :
A ->
A ->
Prop.
Variable lessB :
B ->
B ->
Prop.
Variable eqA_reflexive:
forall a,
eqA a a.
Variable eqA_symmetric:
forall a1 a2,
eqA a1 a2 ->
eqA a2 a1.
Variable eqA_transitive:
forall a1 a2 a3,
eqA a1 a2 ->
eqA a2 a3 ->
eqA a1 a3.
Variable eqA_lessA_compatible:
forall a1 a2 a3,
lessA a1 a2 ->
eqA a2 a3 ->
lessA a1 a3.
Inductive lexprod : (
A *
B) -> (
A *
B) ->
Prop :=
|
LexprodLeft:
forall a1 b1 a2 b2,
lessA a1 a2 ->
lexprod (
a1,
b1) (
a2,
b2)
|
LexprodRight:
forall a1 b1 a2 b2,
eqA a1 a2 ->
lessB b1 b2 ->
lexprod (
a1,
b1) (
a2,
b2).
Lemma lexprod_intro:
forall a1 b1 a2 b2,
(
lessA a1 a2 \/
eqA a1 a2) ->
lessB b1 b2 ->
lexprod (
a1,
b1) (
a2,
b2).
Proof.
Variable wfA :
well_founded lessA.
Variable wfB :
well_founded lessB.
Lemma lexprod_accessibility:
forall a1,
Acc lessA a1 ->
forall b,
Acc lessB b ->
forall a2,
eqA a1 a2 ->
Acc lexprod (
a2,
b).
Proof.
induction 1; induction 1; intros; constructor.
intros ? h. dependent destruction h; eauto.
Qed.
Lemma lexprod_wf:
well_founded lexprod.
Proof.
Variable lessA_eqA_compatible:
forall a1 a2 a3,
eqA a1 a2 ->
lessA a2 a3 ->
lessA a1 a3.
Variable lessA_transitive:
forall a1 a2 a3,
lessA a1 a2 ->
lessA a2 a3 ->
lessA a1 a3.
Variable lessB_transitive:
forall b1 b2 b3,
lessB b1 b2 ->
lessB b2 b3 ->
lessB b1 b3.
Lemma lexprod_transitive:
forall ab1 ab2 ab3,
lexprod ab1 ab2 ->
lexprod ab2 ab3 ->
lexprod ab1 ab3.
Proof.
introv h1 h2. dependent destruction h1; dependent destruction h2; try solve [ left; eauto 2 | right; eauto 2 ].
Qed.
End lexicographic_product.
Hint Constructors lexprod.
The following tactic helps prove goals of the form lexprod _ _.
It is parameterized with four tactics for proving simpler goals.
Ltac lexprod eqA ltA ltB leA :=
solve [
left;
eqA |
right; [
ltA |
ltB ] |
eapply lexprod_intro; [
leA |
ltB ]].