Ackermann Model of HF

We construct a model of HF using from Coq's library.

Require Import Omega HFS.HF.

Implicit Types x y z : .

Fixpoint x :=
  match x with
  | O O
  | S x' S (S ( x'))
  end.

Fixpoint x :=
  match x with
    |O S O
    |S x ( x)
  end.

Fixpoint x : bool :=
  match x with
  | O false
  | S x negb ( x)
  end.

Fixpoint x :=
  match x with
  | O O
  | S x' if ( x) then x' else S ( x')
  end.

Fixpoint mem x y : bool :=
  match x with
  | O y
  | S x' mem x' ( y)
  end.

Definition adj x y :=
  if mem x y then y else x + y.

Definition without z x :=
  if mem z x then x - z else x.

Arithmetical facts needed

Lemma mul2div2_evenodd x :
   x = false ( x) = x
   x = true S ( ( x)) = x.
Proof.
  induction x.
  - simpl. left. tauto.
  - simpl. destruct IHx as [[ ]|[ ]]; simpl.
    + right. rewrite . now split.
    + left. rewrite . now split.
Qed.


Lemma mod2_add_mul2 x y :
   ( x + y) = y.
Proof.
  induction x as [|x IHx]; [reflexivity | simpl].
  rewrite IHx. now destruct ( y).
Qed.


Lemma div2mul2add x y :
   ( x + y) = x + y.
Proof.
 induction x as [|x IHx]; [reflexivity | simpl].
 rewrite IHx. now destruct ( ( x + y)).
Qed.


Lemma muldiv_smaller x :
  x ( x).
Proof.
  destruct (mul2div2_evenodd x) as [[_ IH]|[_ IH]]; omega.
Qed.


Lemma div2SSlt x :
   (S x) < S x (S (S x)) < S (S x).
Proof.
  induction x as [|x IHx]; simpl in *; [omega |].
  destruct ( x); simpl in *; omega.
Qed.


Lemma div2Slt x :
   (S x) < S x.
Proof.
  generalize (div2SSlt x). tauto.
Qed.


Lemma mul2_larger_S x :
   (S x) > (S x).
Proof.
  induction x; simpl in *; omega.
Qed.


Lemma mul2_larger_pres x y :
  x y x y.
Proof.
  induction 1; simpl; omega.
Qed.


Lemma pow2_larger x :
   x > x.
Proof.
  induction x; simpl; try omega.
  destruct ( x) as [|n]; [omega |].
  pose proof mul2_larger_S n as H'. omega.
Qed.


HF induction

Lemma emptyEq x :
  mem x O = false.
Proof.
  induction x; auto.
Qed.


Lemma mem_smaller x y :
  mem x y = true x y.
Proof.
  revert y. induction x as [|x IHx].
  - intros [|y]; simpl in *. discriminate. omega.
  - intros y A. simpl in *. specialize (IHx _ A).
    apply mul2_larger_pres in IHx. assert (H := muldiv_smaller y). omega.
Qed.


Lemma mem_add x y :
  mem x ( x + y) = negb (mem x y).
Proof.
  revert y.
  induction x as [|x IHx]; intros y; simpl;
    [reflexivity | now rewrite div2mul2add].
Qed.


Lemma complete_induction (p : Type) :
  ( x, ( y, y < x p y) p x) x, p x.
Proof.
  intros H x. apply H.
  induction x as [|x IHx]; intros y .
  - omega.
  - destruct (lt_eq_lt_dec x y) as [[A| ]|A].
    omega. now apply H. now apply IHx.
Qed.


Lemma dec_empty y :
  (y = O) + x, mem x y = true.
Proof.
  pattern y. revert y. apply complete_induction.
  intros [|y].
  - now left.
  - intros IH. right. destruct (IH _ (div2Slt y)) as [IHA|(x&B)].
    + destruct y as [|y]. now exists O.
      simpl in IHA. destruct ( y); discriminate IHA.
    + now exists (S x).
Qed.


Lemma without_inverse z x :
  mem z x = true adj z (without z x) = x.
Proof.
  unfold adj, without. intros A. rewrite !A.
  pose proof le_plus_minus _ _ (mem_smaller A) as H.
  rewrite H, mem_add in A. now destruct (mem z (x - z)).
Qed.


Fact sip (p: Type) :
  p O ( x y, p x p y p (adj x y)) x, p x.
Proof.
  intros base IH x.
  pattern x. revert x. apply complete_induction.
  intros y IH'. destruct (dec_empty y) as [ | (x & A)].
  - assumption.
  - rewrite (without_inverse A). pose (H := pow2_larger x). apply IH.
    + apply IH'. apply mem_smaller in A. omega.
    + apply IH'. destruct y as [|y].
      now rewrite emptyEq in A. unfold without. rewrite A. omega.
Qed.


Remaining HF laws

Lemma adj_mem x y :
  mem x (adj x y) = true.
Proof.
  unfold adj. case_eq (mem x y). trivial.
  rewrite mem_add. now intros .
Qed.


Lemma adj_diff z x y :
  z x mem z (adj x y) = mem z y.
Proof.
  revert x y. unfold adj. induction z as [|z IHz].
  - intros [|x] y A. now contradiction A.
    simpl. destruct (mem x ( y)). reflexivity.
    now rewrite mod2_add_mul2.
  - destruct x as [|x]; intros y A; simpl.
    + case_eq ( y); simpl; now try intros .
    + assert (z x) by congruence.
      specialize (IHz _ ( y) H).
      destruct (mem x ( y)); [reflexivity |now rewrite div2mul2add].
Qed.


Fact cancel x y :
  adj x (adj x y) = adj x y.
Proof.
  unfold adj at 1. now rewrite (adj_mem x y).
Qed.


Instance nat_eq_dec :
  eq_dec .
Proof.
  intros x y. hnf. decide equality.
Qed.


Fact swap x y z :
  adj x (adj y z) = adj y (adj x z).
Proof.
  unfold adj at 1 3.
  decide (x = y) as [ |e]. reflexivity.
  rewrite !adj_diff; try congruence.
  unfold adj. destruct (mem x z); destruct (mem y z); omega.
Qed.


Fact disjoint x y :
  adj x y O.
Proof.
  intros A. assert (H := adj_mem x y).
  now rewrite A, emptyEq in H.
Qed.


Lemma mem_adj_iff x y :
  mem x y = true adj x y = y.
Proof.
  unfold adj. split.
  - now intros .
  - destruct (mem x y). reflexivity.
    pose proof pow2_larger x as H. omega.
Qed.


Fact membership z x y :
  adj z (adj x y) = adj x y z = x adj z y = y.
Proof.
  rewrite !mem_adj_iff. intros A.
  decide (z = x) as [ |B]. now left.
  right. now rewrite (adj_diff y B).
Qed.


Model construction