Как доказать разрешимость отношения, меняющего его параметры?

У меня есть ситуация, когда я определил индуктивный тип данных t и частичный заказ le за это (ср le_refl, le_trans, а также le_antisym). Орден имеет эту особенность в le_C В этом случае порядок аргументов поменялся местами в индуктивной гипотезе.

Из-за этого мне не удалось доказать, что это отношение порядка является детерминированным (ср. le_dec). Проблемная подзадача заключается в следующем.

1 subgoal
t1 : t
IHt1 : forall t2 : t, {le t1 t2} + {~ le t1 t2}
t2 : t
______________________________________(1/1)
{le (C t1) (C t2)} + {~ le (C t1) (C t2)}

Гипотеза индукции относится к le t1 t2 пока мне нужно le t2 t1,

Когда я думаю об этом, имеет смысл, что эта двоичная функция не является примитивно рекурсивной ни по первому, ни по второму параметру, а скорее по паре обоих аргументов. У меня сложилось впечатление, что я должен как-то сделать индукцию по обоим аргументам одновременно, но не понимаю, как это сделать.

Мне удалось определить булеву функцию leb и использовать это, чтобы доказать le_dec, но мне интересно, с точки зрения изучения, как сделать доказательство непосредственно с индукцией.

Вопросы

  1. Как я могу прямо доказать le_dec основанный на определении le (т.е. без предварительного определения эквивалентной логической функции)?

Минимальный исполняемый пример

Основные определения

Inductive t : Set :=
  | A : t
  | B : t -> t
  | C : t -> t
  .

Inductive le : t -> t -> Prop :=
  | le_A :
      le A A

  | le_B : forall x y,
      le x y -> le (B x) (B y)

  | le_C : forall x y,
      le y x -> le (C x) (C y)

  | le_trans : forall t1 t2 t3,
      le t1 t2 -> le t2 t3 -> le t1 t3
  .

Хелпер леммы

Require Import Coq.Program.Equality.

Lemma le_canonical_form_A_left (t1 : t) :
  le A t1 -> t1 = A.
Proof.
  intros LE. dependent induction LE; auto.
Qed.

Lemma le_canonical_form_B_left (t1 t2 : t) :
  le (B t1) t2 -> exists t3, t2 = B t3.
Proof.
  intros LE. dependent induction LE.
  - eauto.
  - destruct IHLE1 with t1 as [t4 ?]; clear IHLE1; trivial; subst.
    destruct IHLE2 with t4 as [t4' ?]; clear IHLE2; trivial; subst. eauto.
Qed.

Lemma le_canonical_form_C_left (t1 t2 : t) :
  le (C t1) t2 -> exists t3, t2 = C t3.
Proof.
  intros LE. dependent induction LE.
  - eauto.
  - destruct IHLE1 with t1 as [t4 ?]; clear IHLE1; trivial; subst.
    destruct IHLE2 with t4 as [t4' ?]; clear IHLE2; trivial; subst. eauto.
Qed.

Lemma le_inversion_B (t1 t2 : t) :
  le (B t1) (B t2) -> le t1 t2.
Proof.
  intros LE.
  dependent induction LE.
  - assumption.
  - apply le_canonical_form_B_left in LE1 as [t3 ?]; subst. eauto using le_trans.
Qed.

Lemma le_inversion_C (t1 t2 : t) :
  le (C t1) (C t2) -> le t2 t1.
Proof.
  intros LE.
  dependent induction LE.
  - assumption.
  - apply le_canonical_form_C_left in LE1 as [t3 ?]; subst. eauto using le_trans.
Qed.

Lemma le_inversion (t1 t2 : t) :
  le t1 t2 ->
  t1 = A /\ t2 = A \/
  (exists t1' t2', t1 = B t1' /\ t2 = B t2') \/
  (exists t1' t2', t1 = C t1' /\ t2 = C t2').
Proof.
  intros LE.
  destruct t1.
  - apply le_canonical_form_A_left in LE; subst. auto.
  - apply le_canonical_form_B_left in LE as [? ?]; subst. eauto 6.
  - apply le_canonical_form_C_left in LE as [? ?]; subst. eauto 6.
Qed.

Доказательства частичного заказа

Lemma le_refl (x : t) :
  le x x.
Proof.
  induction x; eauto using le.
Qed.    

Lemma le_antisym (t1 t2 : t) :
  le t1 t2 -> le t2 t1 -> t1 = t2.
Proof.
  induction 1; intros LE.
  - auto.
  - apply le_inversion_B in LE. f_equal; auto.
  - apply le_inversion_C in LE. f_equal; auto using eq_sym.
  - rewrite IHle1; eauto using le_trans.
Qed.

Эквивалентная булева функция

Fixpoint height (x : t) : nat :=
  match x with
  | A => 1
  | B x' => 1 + height x'
  | C x' => 1 + height x'
  end.

Definition height_pair (p : t * t) : nat :=
  let (t1, t2) := p in height t1 + height t2.

Require Import Recdef.
Require Import Omega.

Function leb (p : t * t) { measure height_pair p } : bool :=
  match p with
  | (A, A) => true
  | (B x', B y') => leb (x', y')
  | (C x', C y') => leb (y', x')
  | _ => false
  end.
  - intros. subst. simpl. omega.
  - intros. subst. simpl. omega.
Defined.

Ltac inv H := inversion H; clear H; subst.

Lemma le_to_leb (t1 t2 : t) :
  le t1 t2 -> leb (t1, t2) = true.
Proof.
  remember (t1, t2) as p eqn:Heqn.
  revert Heqn.
  revert t1 t2.
  functional induction (leb p); intros t1 t2 Heqn LE; inv Heqn.
  - trivial.
  - apply IHb with x' y'; trivial.
    now apply le_inversion_B in LE.
  - apply IHb with y' x'; trivial.
    now apply le_inversion_C in LE.
  - exfalso. apply le_inversion in LE.
    intuition; subst.
    + easy.
    + destruct H0.
      destruct H.
      now (intuition; subst).
    + destruct H0.
      destruct H.
      now (intuition; subst).
Qed.

Lemma leb_to_le (t1 t2 : t) :
  leb (t1, t2) = true -> le t1 t2.
Proof.
  remember (t1, t2) as p eqn:Heqn.
  revert Heqn.
  revert t1 t2.
  functional induction (leb p); intros t1 t2 Heqn LEB; inv Heqn.
  - eauto using le.
  - eauto using le.
  - eauto using le.
  - discriminate LEB.
Qed.

Corollary le_iff_leb (t1 t2 : t) :
  le t1 t2 <-> leb (t1, t2) = true.
Proof.
  split.
  - apply le_to_leb.
  - apply leb_to_le.
Qed.

Что я на самом деле хочу доказать

Lemma le_dec (t1 t2 : t) :
  { le t1 t2 } + { ~le t1 t2 }.
Proof.
  revert t2.
  induction t1; intros t2.
  - destruct t2.
    + eauto using le.
    + right. intro contra. dependent induction contra.
      apply le_canonical_form_A_left in contra1; subst. eauto.
    + right. intro contra. dependent induction contra.
      apply le_canonical_form_A_left in contra1; subst. eauto.
  - destruct t2.
    + right. intro contra. clear IHt1. dependent induction contra.
      apply le_canonical_form_B_left in contra1 as [? ?]; subst. eauto.
    + destruct IHt1 with t2.
      * eauto using le.
      * right. intro contra. apply le_inversion_B in contra. contradiction.
    + right; intro contra. clear IHt1. dependent induction contra.
      apply le_canonical_form_B_left in contra1 as [? ?]; subst. eauto.
  - destruct t2.
    + right. intro contra. clear IHt1. dependent induction contra.
      apply le_canonical_form_C_left in contra1 as [? ?]; subst. eauto.
    + right. intro contra. clear IHt1. dependent induction contra.
      apply le_canonical_form_C_left in contra1 as [? ?]; subst. eauto.
    + destruct IHt1 with t2.
      * admit. (* Wrong assumption *)
      * admit. (* Wrong assumption *)
Restart.
  destruct (leb (t1, t2)) eqn:Heqn.
  - apply leb_to_le in Heqn. auto.
  - right. intro contra. apply le_to_leb in contra.
    rewrite Heqn in contra. discriminate.
Qed.

Решение основано на ответе Артура

Ltac destruct_exs_conjs :=
  repeat match goal with
  | H : exists _, _ |- _ => destruct H
  | H : _ /\ _ |- _ => destruct H
  end; subst.

Lemma le_dec_aux (t1 t2 : t) (n : nat) :
  height t1 + height t2 <= n ->
  {le t1 t2} + {~le t1 t2}.
Proof.
  revert t1 t2.
  induction n as [| n IH]; intros t1 t2 H.
  - destruct t1; simpl in H; omega.
  - destruct t1, t2.
    + eauto using le.
    + clear. right. intro contra. dependent induction contra.
      apply le_canonical_form_A_left in contra1; subst. eauto.
    + clear. right. intro contra. dependent induction contra.
      apply le_canonical_form_A_left in contra1; subst. eauto.
    + clear. right. intro contra. dependent induction contra.
      apply le_canonical_form_B_left in contra1; destruct_exs_conjs. eauto.
    + simpl in H.
      destruct (IH t1 t2); try omega.
      * eauto using le.
      * right. intro contra. apply le_inversion_B in contra. contradiction.
    + clear. right. intro contra. dependent induction contra.
      apply le_canonical_form_B_left in contra1; destruct_exs_conjs. eauto.
    + clear. right. intro contra. dependent induction contra.
      apply le_canonical_form_C_left in contra1; destruct_exs_conjs. eauto.
    + clear. right. intro contra. dependent induction contra.
      apply le_canonical_form_C_left in contra1; destruct_exs_conjs. eauto.
    + simpl in H.
      destruct (IH t2 t1); try omega.
      * eauto using le.
      * right. intro contra. apply le_inversion_C in contra. contradiction.
Qed.

Lemma le_dec' (t1 t2 : t) :
  { le t1 t2 } + { ~le t1 t2 }.
Proof.
  destruct (le_dec_aux t1 t2 (height t1 + height t2)); auto.
Qed.
Источник

2 ответа

Решение

Аналогично тому, что вы использовали для определения leb функция, вам нужно доказать le_dec по индукции по высоте элементов:

Lemma le_dec_aux t1 t2 n : height t1 + height t2 <= n -> {le t1 t2} + {~le t1 t2}.
Proof.
revert t1 t2.
induction n as [|n IH].
(* ... *)

При этом, я думаю, что это прекрасно, чтобы доказать разрешимость, используя булеву функцию. Библиотека математических компонентов широко использует этот шаблон, используя специализированные reflect Предикат для соединения общих предложений с логическими вычислениями, вместо sumbool тип {A} + {B},

Источник

Я попробовал версию, предложенную @Arthur, используя обоснованную рекурсию. Это действительно дает хорошее извлечение.

Definition rel p1 p2 := height_pair p1 < height_pair p2.

Lemma rel_wf : well_founded rel.
Proof.
  apply well_founded_ltof.
Qed.

Lemma le_dec (t1 t2 : t) :
  { le t1 t2 } + { ~le t1 t2 }.
Proof.
  induction t1, t2 as [t1 t2]
    using (fun P => well_founded_induction_type_2 P rel_wf).
  destruct t1, t2;
    try (right; intros contra;
         (apply le_canonical_form_A_left in contra)
      || (apply le_canonical_form_B_left in contra; destruct contra)
      || (apply le_canonical_form_C_left in contra; destruct contra);
      discriminate).
  - left. apply le_A.
  - destruct (H t1 t2).
    + unfold rel, height_pair; simpl. omega.
    + left. apply le_B. assumption.
    + right. intros contra. apply le_inversion_B in contra. contradiction.
  - destruct (H t2 t1).
    + unfold rel, height_pair; simpl. omega.
    + left. apply le_C. assumption.
    + right. intros contra. apply le_inversion_C in contra. contradiction.
Qed.

Extraction Inline well_founded_induction_type_2 Fix_F_2.
  (* to have a nice extraction *)
Extraction le_dec.

Обратите внимание, однако, что определенное вами отношение порядка на самом деле является просто отношением равенства, но, возможно, вы описали упрощение вашего первоначального варианта использования.

Lemma le_is_eq : forall t1 t2, le t1 t2 -> t1 = t2.
Proof.
  intros.
  induction t1, t2 as [t1 t2]
    using (fun P => well_founded_induction_type_2 P rel_wf).
  destruct t1, t2;
    try ((apply le_canonical_form_A_left in H)
      || (apply le_canonical_form_B_left in H; destruct H)
      || (apply le_canonical_form_C_left in H; destruct H);
      discriminate).
  - reflexivity.
  - apply le_inversion_B in H.
    apply H0 in H.
    + congruence.
    + unfold rel, height_pair. simpl. omega.
  - apply le_inversion_C in H.
    apply H0 in H.
    + congruence.
    + unfold rel, height_pair. simpl. omega.
Qed.
Источник
Другие вопросы по тегам