# HpropHeap Predicates

Set Implicit Arguments.

From SLF Require Export LibSepReference.

Import ProgramSyntax.

From SLF Require Export LibSepReference.

Import ProgramSyntax.

Tweak to simplify the use of definitions and lemmas from LibSepFmap.v.

Arguments Fmap.single {A} {B}.

Arguments Fmap.union {A} {B}.

Arguments Fmap.disjoint {A} {B}.

Arguments Fmap.union_comm_of_disjoint {A} {B}.

Arguments Fmap.union_empty_l {A} {B}.

Arguments Fmap.union_empty_r {A} {B}.

Arguments Fmap.union_assoc {A} {B}.

Arguments Fmap.disjoint_empty_l {A} {B}.

Arguments Fmap.disjoint_empty_r {A} {B}.

Arguments Fmap.disjoint_union_eq_l {A} {B}.

Arguments Fmap.disjoint_union_eq_r {A} {B}.

Arguments Fmap.union {A} {B}.

Arguments Fmap.disjoint {A} {B}.

Arguments Fmap.union_comm_of_disjoint {A} {B}.

Arguments Fmap.union_empty_l {A} {B}.

Arguments Fmap.union_empty_r {A} {B}.

Arguments Fmap.union_assoc {A} {B}.

Arguments Fmap.disjoint_empty_l {A} {B}.

Arguments Fmap.disjoint_empty_r {A} {B}.

Arguments Fmap.disjoint_union_eq_l {A} {B}.

Arguments Fmap.disjoint_union_eq_r {A} {B}.

# First Pass

- A location has type loc.
- A value has type val.
- A state has type state.

- H denotes a heap predicate of type hprop; it describes a piece of state,
- Q denotes a postcondition, of type val→hprop; it describes both a result value and a piece of state. Observe that val→hprop is equivalent to val→state→Prop.

- \[] denotes the empty heap predicate,
- \[P] denotes a pure fact,
- p ~~> v denotes a singleton heap,
- H
_{1}\* H_{2}denotes the separating conjunction, - Q
_{1}\*+ H_{2}denotes the separating conjunction, between a postcondition and a heap predicate, - \∃ x, H denotes an existential.

- a Hoare triple, written hoare t H Q, features a precondition H and a postcondition Q that describe the whole memory state in which the execution of the term t takes place.
- a Separation Logic triple, written triple t H Q, features a pre- and a postcondition that describes only the piece of the memory state in which the execution of the term t takes place.

- applys is an enhanced version of eapply.
- applys_eq is a variant of applys that enables matching the arguments of the predicate that appears in the goal "up to equality" rather than "up to conversion".
- specializes is an enhanced version of specialize.
- lets and forwards are forward-chaining tactics that enable instantiating a lemma.

## Syntax and Semantics

- a type of terms, written trm,
- a type of values, written val,
- a type of states, written state (i.e., finite map from loc to val),
- a big-step evaluation judgment, written eval h
_{1}t h_{2}v, asserting that, starting from state s_{1}, the evaluation of the term t terminates in the state s_{2}and produces the value v.

Check eval : state → trm → state → val → Prop.

Definition example_val : val :=

val_fun "x" (trm_if (trm_var "x") (trm_val (val_int 0)) (trm_val (val_int 1))).

val_fun "x" (trm_if (trm_var "x") (trm_val (val_int 0)) (trm_val (val_int 1))).

Thanks to a set of coercions and notation, this term can be written in a
somewhat more readable way, as follows.

Definition example_val' : trm :=

<{ fun "x" ⇒

if "x" then 0 else 1 }>.

<{ fun "x" ⇒

if "x" then 0 else 1 }>.

## Description of the State

Definition state : Type := fmap loc val.

By convention, we use the type state describes a full state of memory,
and introduce the type heap to describe just a piece of state.

Definition heap : Type := state.

In particular, the library LibSepFmap.v, whose module name is abbreviated
as Fmap, exports the following definitions.
The types of these definitions are as follows.

Check Fmap.empty : heap.

Check Fmap.single : loc → val → heap.

Check Fmap.union : heap → heap → heap.

Check Fmap.disjoint : heap → heap → Prop.
Note that the union operation is commutative only when its two arguments
have disjoint domains. Throughout the Separation Logic course, we will
only consider disjoint unions, for which commutativity holds.

- Fmap.empty denotes the empty state,
- Fmap.single p v denotes a singleton state, that is, a unique cell at location p with contents v,
- Fmap.union h
_{1}h_{2}denotes the union of the two states h_{1}and h_{2}. - Fmap.disjoint h
_{1}h_{2}asserts that h_{1}and h_{2}have disjoint domains.

Check Fmap.empty : heap.

Check Fmap.single : loc → val → heap.

Check Fmap.union : heap → heap → heap.

Check Fmap.disjoint : heap → heap → Prop.

## Heap Predicates

Definition hprop := heap → Prop.

Thereafter, let H range over heap predicates.

Implicit Type H : hprop.

An essential aspect of Separation Logic is that all heap predicates
defined and used in practice are built using a few basic combinators.
In other words, except for the definition of the combinators themselves,
we will never define a custom heap predicate directly as a function
of the state.
We next describe the most important combinators of Separation Logic.
The hempty predicate, usually written \[], characterizes an empty
state.

Definition hempty : hprop :=

fun (h:heap) ⇒ (h = Fmap.empty).

Notation "\[]" := (hempty) (at level 0).

fun (h:heap) ⇒ (h = Fmap.empty).

Notation "\[]" := (hempty) (at level 0).

The pure fact predicate, written \[P], characterizes an empty state
and moreover asserts that the proposition P is true.

Definition hpure (P:Prop) : hprop :=

fun (h:heap) ⇒ (h = Fmap.empty) ∧ P.

Notation "\[ P ]" := (hpure P) (at level 0, format "\[ P ]").

fun (h:heap) ⇒ (h = Fmap.empty) ∧ P.

Notation "\[ P ]" := (hpure P) (at level 0, format "\[ P ]").

The singleton heap predicate, written p ~~> v, characterizes a
state with a single allocated cell, at location p, storing the
value v.

Definition hsingle (p:loc) (v:val) : hprop :=

fun (h:heap) ⇒ (h = Fmap.single p v).

Notation "p '~~>' v" := (hsingle p v) (at level 32).

fun (h:heap) ⇒ (h = Fmap.single p v).

Notation "p '~~>' v" := (hsingle p v) (at level 32).

The "separating conjunction", written H

_{1}\* H_{2}, characterizes a state that can be decomposed in two disjoint parts, one that satisfies H_{1}, and another that satisfies H_{2}. In the definition below, the two parts are named h_{1}and h_{2}.
Definition hstar (H

fun (h:heap) ⇒ ∃ h

∧ H

∧ Fmap.disjoint h

∧ h = Fmap.union h

Notation "H

_{1}H_{2}: hprop) : hprop :=fun (h:heap) ⇒ ∃ h

_{1}h_{2}, H_{1}h_{1}∧ H

_{2}h_{2}∧ Fmap.disjoint h

_{1}h_{2}∧ h = Fmap.union h

_{1}h_{2}.Notation "H

_{1}'\*' H_{2}" := (hstar H_{1}H_{2}) (at level 41, right associativity).
The existential quantifier for heap predicates, written \∃ x, H
characterizes a heap that satisfies H for some x.
The variable x has type A, for some arbitrary type A.
The notation \∃ x, H stands for hexists (fun x ⇒ H).
The generalized notation \∃ x
The definition of hexists is a bit technical. It is not essential
to master it at this point. Additional explanations are provided
near the end of this chapter.

_{1}... xn, H is also available.
Definition hexists (A:Type) (J:A→hprop) : hprop :=

fun (h:heap) ⇒ ∃ x, J x h.

Notation "'\exists' x

(hexists (fun x

(at level 39, x

format "'[' '\exists' '/ ' x

fun (h:heap) ⇒ ∃ x, J x h.

Notation "'\exists' x

_{1}.. xn , H" :=(hexists (fun x

_{1}⇒ .. (hexists (fun xn ⇒ H)) ..))(at level 39, x

_{1}binder, H at level 50, right associativity,format "'[' '\exists' '/ ' x

_{1}.. xn , '/ ' H ']'").
All the definitions above are eventually turned Opaque, after
the appropriate introduction and elimination lemmas are
established for them. Thus, at some point it is no longer
possible to involve, say unfold hstar. Opacity ensures that
all the proofs that are constructed do not depend on the
details of how these definitions of heap predicates are set up.

## Extensionality for Heap Predicates

Parameter hstar_assoc : ∀ H

(H

_{1}H_{2}H_{3},(H

_{1}\* H_{2}) \* H_{3}= H_{1}\* (H_{2}\* H_{3}).
How can we prove a goal of the form H
Intuitively, H and H' are equal if and only if they
characterize exactly the same set of heaps, that is, if
∀ (h:heap), H
This reasoning principle, a specific form of extensionality
property, is not available by default in Coq. But we can safely
assume it if we extend the logic of Coq with a standard axiom
called "predicate extensionality".

_{1}= H_{2}when H_{1}and H_{2}have type hprop, that is, heap→Prop?_{1}h ↔ H_{2}h.
Axiom predicate_extensionality : ∀ (A:Type) (P Q:A→Prop),

(∀ x, P x ↔ Q x) →

P = Q.

(∀ x, P x ↔ Q x) →

P = Q.

By specializing P and Q above to the type hprop, we obtain
exactly the desired extensionality principle.

Lemma hprop_eq : ∀ (H

(∀ (h:heap), H

H

Proof using. applys predicate_extensionality. Qed.

_{1}H_{2}:hprop),(∀ (h:heap), H

_{1}h ↔ H_{2}h) →H

_{1}= H_{2}.Proof using. applys predicate_extensionality. Qed.

## Type and Syntax for Postconditions

Implicit Type Q : val → hprop.

One common operation is to augment a postcondition with a piece of state.
This operation is described by the operator Q \*+ H, which is just a
convenient notation for fun x ⇒ (Q x \* H).

Notation "Q \*+ H" := (fun x ⇒ hstar (Q x) H) (at level 40).

Intuitively, in order to prove that two postconditions Q
Again, the extensionality property that we need is not built-in to Coq.
We need the axiom called "functional extensionality", stated next.

_{1}and Q_{2}are equal, it suffices to show that the heap predicates Q_{1}v and Q_{2}v (both of type hprop) are equal for any value v.
Axiom functional_extensionality : ∀ A B (f g:A→B),

(∀ x, f x = g x) →

f = g.

(∀ x, f x = g x) →

f = g.

The desired equality property for postconditions follows directly
from that axiom.

Lemma qprop_eq : ∀ (Q

(∀ (v:val), Q

Q

Proof using. applys functional_extensionality. Qed.

_{1}Q_{2}:val→hprop),(∀ (v:val), Q

_{1}v = Q_{2}v) →Q

_{1}= Q_{2}.Proof using. applys functional_extensionality. Qed.

## Separation Logic Triples and the Frame Rule

Definition hoare (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (s:state), H s →

∃ (s':state) (v:val), eval s t s' v ∧ Q v s'.

∀ (s:state), H s →

∃ (s':state) (v:val), eval s t s' v ∧ Q v s'.

Note that Q has type val→hprop, thus Q v has type hprop.
Recall that hprop = heap→Prop. Thus Q v s' has type Prop.
The frame rule asserts that if one can derive a specification of
the form triple H t Q for a term t, then one should be able
to automatically derive triple (H \* H') t (Q \*+ H') for any H'.
Intuitively, if t executes safely in a heap H, it should behave
similarly in any extension of H with a disjoint part H'. Moreover,
its evaluation should leave this piece of state H' unmodified
throughout the execution of t.
The following definition of a Separation Logic triple builds upon
that of a Hoare triple by "baking in" the frame rule.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').

This definition inherently satisfies the frame rule, as we show
below. The proof only exploits the associativity of the star
operator.

Lemma triple_frame : ∀ t H Q H',

triple t H Q →

triple t (H \* H') (Q \*+ H').

Proof using.

introv M. unfold triple in *. rename H' into H

specializes M (H

(* M matches the goal up to rewriting for associativity. *)

applys_eq M.

{ rewrite hstar_assoc. auto. }

{ applys functional_extensionality. intros v. rewrite hstar_assoc. auto. }

Qed.

triple t H Q →

triple t (H \* H') (Q \*+ H').

Proof using.

introv M. unfold triple in *. rename H' into H

_{1}. intros H_{2}.specializes M (H

_{1}\* H_{2}).(* M matches the goal up to rewriting for associativity. *)

applys_eq M.

{ rewrite hstar_assoc. auto. }

{ applys functional_extensionality. intros v. rewrite hstar_assoc. auto. }

Qed.

## Example of a Triple: the Increment Function

Parameter incr : val.

An application of this function, written incr p, is technically
a term of the form trm_app (trm_val incr) (trm_val (val_loc p)),
where trm_val injects values in the grammar of terms, and
val_loc injects locations in the grammar of locations.
The abbreviation incr p parses correctly because trm_app,
trm_val, and val_loc are registered as coercions. Let us
check this claim with Coq.

Lemma incr_applied : ∀ (p:loc) (n:int),

trm_app (trm_val incr) (trm_val (val_loc p))

= incr p.

Proof using. reflexivity. Qed.

trm_app (trm_val incr) (trm_val (val_loc p))

= incr p.

Proof using. reflexivity. Qed.

The operation incr p is specified using a triple as shown
below.

Parameter triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun r ⇒ p ~~> (n+1)).

triple (trm_app incr p)

(p ~~> n)

(fun r ⇒ p ~~> (n+1)).

## Example Applications of the Frame Rule

Lemma triple_incr_2 : ∀ (p q:loc) (n m:int),

triple (incr p)

((p ~~> n) \* (q ~~> m))

(fun _ ⇒ (p ~~> (n+1)) \* (q ~~> m)).

triple (incr p)

((p ~~> n) \* (q ~~> m))

(fun _ ⇒ (p ~~> (n+1)) \* (q ~~> m)).

The above specification lemma is derivable from the specification
lemma triple_incr by applying the frame rule to augment
both the precondition and the postcondition with q ~~> m.

Proof using.

intros. lets M: triple_incr p n.

lets N: triple_frame (q ~~> m) M. apply N.

Qed.

intros. lets M: triple_incr p n.

lets N: triple_frame (q ~~> m) M. apply N.

Qed.

Here, we have framed on q ~~> m, but we could similarly
frame on any heap predicate H, as captured by the following
specification lemma.

Parameter triple_incr_3 : ∀ (p:loc) (n:int) (H:hprop),

triple (incr p)

((p ~~> n) \* H)

(fun _ ⇒ (p ~~> (n+1)) \* H).

triple (incr p)

((p ~~> n) \* H)

(fun _ ⇒ (p ~~> (n+1)) \* H).

Remark: in practice, we always prefer writing
"small-footprint specifications", such as triple_incr,
that describe the minimal piece of state necessary for
the function to execute. Indeed, other specifications that
describe a larger piece of state can be derived by application
of the frame rule.

## Power of the Frame Rule with Respect to Allocation

Parameter triple_ref : ∀ (v:val),

triple (val_ref v)

\[]

(funloc p ⇒ p ~~> v).

triple (val_ref v)

\[]

(funloc p ⇒ p ~~> v).

Applying the frame rule to the above specification, and to
another memory cell, say l' ~~> v', we obtain:

Parameter triple_ref_with_frame : ∀ (l':loc) (v':val) (v:val),

triple (val_ref v)

(l' ~~> v')

(funloc p ⇒ p ~~> v \* l' ~~> v').

triple (val_ref v)

(l' ~~> v')

(funloc p ⇒ p ~~> v \* l' ~~> v').

This derived specification captures the fact that the newly
allocated cell at address p is distinct from the previously
allocated cell at address l'.
More generally, through the frame rule, we can derive that
any piece of freshly allocated data is distinct from any
piece of previously existing data.
This independence principle is extremely powerful. It is an
inherent strength of Separation Logic.

## Notation for Heap Union

Notation "h

_{1}\u h_{2}" := (Fmap.union h_{1}h_{2}) (at level 37, right associativity).## Introduction and Inversion Lemmas for Basic Operators

Implicit Types P : Prop.

Implicit Types v : val.

Implicit Types v : val.

The introduction lemmas show how to prove goals of the form H h,
for various forms of the heap predicate H.

Lemma hempty_intro :

\[] Fmap.empty.

Proof using. hnf. auto. Qed.

Lemma hpure_intro : ∀ P,

P →

\[P] Fmap.empty.

Proof using. introv M. hnf. auto. Qed.

Lemma hsingle_intro : ∀ p v,

(p ~~> v) (Fmap.single p v).

Proof using. intros. hnf. auto. Qed.

Lemma hstar_intro : ∀ H

H

H

Fmap.disjoint h

(H

Proof using. intros. ∃* h

Lemma hexists_intro : ∀ A (x:A) (J:A→hprop) h,

J x h →

(\∃ x, J x) h.

Proof using. introv M. hnf. eauto. Qed.

\[] Fmap.empty.

Proof using. hnf. auto. Qed.

Lemma hpure_intro : ∀ P,

P →

\[P] Fmap.empty.

Proof using. introv M. hnf. auto. Qed.

Lemma hsingle_intro : ∀ p v,

(p ~~> v) (Fmap.single p v).

Proof using. intros. hnf. auto. Qed.

Lemma hstar_intro : ∀ H

_{1}H_{2}h_{1}h_{2},H

_{1}h_{1}→H

_{2}h_{2}→Fmap.disjoint h

_{1}h_{2}→(H

_{1}\* H_{2}) (h_{1}\u h_{2}).Proof using. intros. ∃* h

_{1}h_{2}. Qed.Lemma hexists_intro : ∀ A (x:A) (J:A→hprop) h,

J x h →

(\∃ x, J x) h.

Proof using. introv M. hnf. eauto. Qed.

The inversion lemmas show how to extract information from hypotheses
of the form H h, for various forms of the heap predicate H.

Lemma hempty_inv : ∀ h,

\[] h →

h = Fmap.empty.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hpure_inv : ∀ P h,

\[P] h →

P ∧ h = Fmap.empty.

Proof using. introv M. hnf in M. autos*. Qed.

Lemma hsingle_inv: ∀ p v h,

(p ~~> v) h →

h = Fmap.single p v.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hstar_inv : ∀ H

(H

∃ h

Proof using. introv M. hnf in M. eauto. Qed.

Lemma hexists_inv : ∀ A (J:A→hprop) h,

(\∃ x, J x) h →

∃ x, J x h.

Proof using. introv M. hnf in M. eauto. Qed.

\[] h →

h = Fmap.empty.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hpure_inv : ∀ P h,

\[P] h →

P ∧ h = Fmap.empty.

Proof using. introv M. hnf in M. autos*. Qed.

Lemma hsingle_inv: ∀ p v h,

(p ~~> v) h →

h = Fmap.single p v.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hstar_inv : ∀ H

_{1}H_{2}h,(H

_{1}\* H_{2}) h →∃ h

_{1}h_{2}, H_{1}h_{1}∧ H_{2}h_{2}∧ Fmap.disjoint h_{1}h_{2}∧ h = h_{1}\u h_{2}.Proof using. introv M. hnf in M. eauto. Qed.

Lemma hexists_inv : ∀ A (J:A→hprop) h,

(\∃ x, J x) h →

∃ x, J x h.

Proof using. introv M. hnf in M. eauto. Qed.

#### Exercise: 4 stars, standard, especially useful (hstar_hpure_l)

Check Fmap.union_empty_l : ∀ h,

Fmap.empty \u h = h.

Check Fmap.disjoint_empty_l : ∀ h,

Fmap.disjoint Fmap.empty h.

Lemma hstar_hpure_l : ∀ P H h,

(\[P] \* H) h = (P ∧ H h).

Proof using. (* FILL IN HERE *) Admitted.

☐

(\[P] \* H) h = (P ∧ H h).

Proof using. (* FILL IN HERE *) Admitted.

☐

## Alternative, Equivalent Definitions for Separation Logic Triples

_{1}satisfies the precondition H and h

_{2}describes the rest of the state, then the evaluation of t produces a value v in a final state made that can be decomposed between a part h

_{1}' and h

_{2}unchanged, in such a way that v and h

_{1}' together satisfy the postcondition Q. Formally:

Definition triple_lowlevel (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ h

Fmap.disjoint h

H h

∃ h

Fmap.disjoint h

∧ eval (h

∧ Q v h

∀ h

_{1}h_{2},Fmap.disjoint h

_{1}h_{2}→H h

_{1}→∃ h

_{1}' v,Fmap.disjoint h

_{1}' h_{2}∧ eval (h

_{1}\u h_{2}) t (h_{1}' \u h_{2}) v∧ Q v h

_{1}'.
Let us establish the equivalence between this alternative
definition of triple and the original one.

#### Exercise: 4 stars, standard, especially useful (triple_iff_triple_lowlevel)

Prove the equivalence between triple and triple_low_level. Warning: this is probably a very challenging exercise.
Lemma triple_iff_triple_lowlevel : ∀ t H Q,

triple t H Q ↔ triple_lowlevel t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

triple t H Q ↔ triple_lowlevel t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

## Alternative Definitions for Heap Predicates

_{1}= H

_{2}. Recall that lemma hprop_eq enables deriving such equalities by invoking predicate extensionality.

Lemma hempty_eq_hpure_true :

\[] = \[True].

Proof using.

unfold hempty, hpure. apply hprop_eq. intros h. iff Hh.

{ auto. }

{ jauto. }

Qed.

\[] = \[True].

Proof using.

unfold hempty, hpure. apply hprop_eq. intros h. iff Hh.

{ auto. }

{ jauto. }

Qed.

Thus, hempty could be defined in terms of hpure, as hpure True,
written \[True].

Definition hempty' : hprop :=

\[True].

\[True].

The pure fact predicate [\P] is equivalent to the existential
quantification over a proof of P in the empty heap, that is,
to the heap predicate \∃ (p:P), \[].

Lemma hpure_eq_hexists_proof : ∀ P,

\[P] = (\∃ (p:P), \[]).

Proof using.

unfold hempty, hpure, hexists. intros P.

apply hprop_eq. intros h. iff Hh.

{ destruct Hh as (E&p). ∃ p. auto. }

{ destruct Hh as (p&E). auto. }

Qed.

\[P] = (\∃ (p:P), \[]).

Proof using.

unfold hempty, hpure, hexists. intros P.

apply hprop_eq. intros h. iff Hh.

{ destruct Hh as (E&p). ∃ p. auto. }

{ destruct Hh as (p&E). auto. }

Qed.

Thus, hpure could be defined in terms of hexists and hempty, as
hexists (fun (p:P) ⇒ hempty), also written \∃ (p:P), \[].

Definition hpure' (P:Prop) : hprop :=

\∃ (p:P), \[].

\∃ (p:P), \[].

It is useful to minimize the number of combinators, both for elegance
and to reduce the proof effort.
Since we cannot do without hexists, we have a choice between
considering either hpure or hempty as primitive, and the other
one as derived. The predicate hempty is simpler and appears as
more fundamental.
Hence, in the subsequent chapters (and in the CFML tool),
we define hpure in terms of hexists and hempty,
like in the definition of hpure' shown above.
In other words, we assume the definition:

Definition hpure (P:Prop) : hprop :=

\∃ (p:P), \[].

Definition hpure (P:Prop) : hprop :=

\∃ (p:P), \[].

## Additional Explanations for the Definition of \∃

Parameter (p:loc).

Check (\∃ (n:int), p ~~> (val_int n)) : hprop.

Check ex : ∀ A : Type, (A → Prop) → Prop.

Check hexists : ∀ A : Type, (A → hprop) → hprop.

Notation "'exists' x .. y , p" := (ex (fun x ⇒ .. (ex (fun y ⇒ p)) ..))

(at level 200, x binder, right associativity,

format "'[' 'exists' '/ ' x .. y , '/ ' p ']'").

Module Extensionality.

To establish extensionality of entailment, we have used
the predicate extensionality axiom. In fact, this axiom
can be derived by combining the axiom of "functional extensionality"
with another one called "propositional extensionality".
The axiom of "propositional extensionality" asserts that
two propositions that are logically equivalent (in the sense
that they imply each other) can be considered equal.

Axiom propositional_extensionality : ∀ (P Q:Prop),

(P ↔ Q) →

P = Q.

(P ↔ Q) →

P = Q.

The axiom of "functional extensionality" asserts that
two functions are equal if they provide equal result
for every argument.

Axiom functional_extensionality : ∀ A B (f g:A→B),

(∀ x, f x = g x) →

f = g.

(∀ x, f x = g x) →

f = g.

#### Exercise: 1 star, standard, especially useful (predicate_extensionality_derived)

Using the two axioms propositional_extensionality and functional_extensionality, show how to derive predicate_extensionality.
Lemma predicate_extensionality_derived : ∀ A (P Q:A→Prop),

(∀ x, P x ↔ Q x) →

P = Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

(∀ x, P x ↔ Q x) →

P = Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

End Extensionality.

## Historical Notes

(* 2021-01-25 13:22 *)